Theorem eqeq1 2043

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq1	⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))

Proof of Theorem eqeq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2031	. . . . . 6 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2	1	biimpi 113	. . . . 5 ⊢ (A = B → ∀x(x ∈ A ↔ x ∈ B))
3	2	19.21bi 1447	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
4	3	bibi1d 222	. . 3 ⊢ (A = B → ((x ∈ A ↔ x ∈ 𝐶) ↔ (x ∈ B ↔ x ∈ 𝐶)))
5	4	albidv 1702	. 2 ⊢ (A = B → (∀x(x ∈ A ↔ x ∈ 𝐶) ↔ ∀x(x ∈ B ↔ x ∈ 𝐶)))
6		dfcleq 2031	. 2 ⊢ (A = 𝐶 ↔ ∀x(x ∈ A ↔ x ∈ 𝐶))
7		dfcleq 2031	. 2 ⊢ (B = 𝐶 ↔ ∀x(x ∈ B ↔ x ∈ 𝐶))
8	5, 6, 7	3bitr4g 212	1 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1240   = wceq 1242   ∈ wcel 1390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  eqeq1i  2044  eqeq1d  2045  eqeq2  2046  eqeq12  2049  eqtr  2054  eqsb3lem  2137  clelab  2159  neeq1  2213  pm13.18  2280  issetf  2556  sbhypf  2597  vtoclgft  2598  eqvincf  2663  pm13.183  2675  eueq  2706  mob  2717  euind  2722  reuind  2738  eqsbc3  2796  csbhypf  2879  uniiunlem  3022  snjust  3372  elprg  3384  elsncg  3389  rabrsndc  3429  sneqrg  3524  preq12bg  3535  intab  3635  dfiin2g  3681  opthg  3966  copsexg  3972  euotd  3982  elopab  3986  snnex  4147  uniuni  4149  eusv1  4150  reusv3  4158  ordtriexmid  4210  onsucelsucexmidlem1  4213  onsucelsucexmid  4215  regexmidlemm  4217  regexmidlem1  4218  nn0suc  4270  nndceq0  4282  0elnn  4283  elxpi  4304  opbrop  4362  relop  4429  ideqg  4430  elrnmpt  4526  elrnmpt1  4528  elrnmptg  4529  cnveqb  4719  relcoi1  4792  funopg  4877  funcnvuni  4911  fun11iun  5090  fvelrnb  5164  fvmptg  5191  fndmin  5217  eldmrexrn  5251  foelrn  5260  foco2  5261  fmptco  5273  elabrex  5340  abrexco  5341  f1veqaeq  5351  f1oiso  5408  eusvobj2  5441  acexmidlema  5446  acexmidlemb  5447  acexmidlem2  5452  acexmidlemv  5453  oprabid  5480  mpt2fun  5545  elrnmpt2g  5555  elrnmpt2  5556  ralrnmpt2  5557  rexrnmpt2  5558  ovi3  5579  ov6g  5580  ovelrn  5591  caovcang  5604  caovcan  5607  eloprabi  5764  dftpos4  5819  elqsg  6092  qsel  6119  brecop  6132  eroveu  6133  erovlem  6134  th3qlem1  6144  th3q  6147  2dom  6221  fundmen  6222  indpi  6326  nqtri3or  6380  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  mulnnnq0  6432  genipv  6491  genpelvl  6494  genpelvu  6495  addsrmo  6651  mulsrmo  6652  aptisr  6685  ltresr  6716  axcnre  6745  axpre-apti  6749  apreap  7351  apreim  7367  creur  7672  creui  7673  nn1m1nn  7693  nn1gt1  7708  elz  8003  nn0ind-raph  8111  nltpnft  8480  xnegeq  8490  expival  8891  bj-nn0suc0  9384  bj-inf2vnlem1  9400  bj-inf2vnlem2  9401  bj-nn0sucALT  9408