Theorem eqeq1 2028

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 2016	. . . . . 6 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2	1	biimpi 113	. . . . 5 ⊢ (A = B → ∀x(x ∈ A ↔ x ∈ B))
3	2	19.21bi 1432	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
4	3	bibi1d 222	. . 3 ⊢ (A = B → ((x ∈ A ↔ x ∈ 𝐶) ↔ (x ∈ B ↔ x ∈ 𝐶)))
5	4	albidv 1687	. 2 ⊢ (A = B → (∀x(x ∈ A ↔ x ∈ 𝐶) ↔ ∀x(x ∈ B ↔ x ∈ 𝐶)))
6		dfcleq 2016	. 2 ⊢ (A = 𝐶 ↔ ∀x(x ∈ A ↔ x ∈ 𝐶))
7		dfcleq 2016	. 2 ⊢ (B = 𝐶 ↔ ∀x(x ∈ B ↔ x ∈ 𝐶))
8	5, 6, 7	3bitr4g 212	1 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1226   = wceq 1228   ∈ wcel 1374

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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004

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

This theorem is referenced by:  eqeq1i  2029  eqeq1d  2030  eqeq2  2031  eqeq12  2034  eqtr  2039  eqsb3lem  2122  clelab  2144  neeq1  2195  pm13.18  2262  issetf  2538  sbhypf  2578  vtoclgft  2579  eqvincf  2644  pm13.183  2656  eueq  2687  mob  2698  euind  2703  reuind  2719  eqsbc3  2777  csbhypf  2860  uniiunlem  3003  snjust  3353  elprg  3365  elsncg  3370  rabrsndc  3410  sneqrg  3505  preq12bg  3516  intab  3616  dfiin2g  3662  opthg  3947  copsexg  3953  euotd  3963  elopab  3967  snnex  4129  uniuni  4131  eusv1  4132  reusv3  4140  ordtriexmid  4192  onsucelsucexmidlem1  4195  onsucelsucexmid  4197  regexmidlemm  4199  regexmidlem1  4200  nn0suc  4252  nndceq0  4264  0elnn  4265  elxpi  4286  opbrop  4344  relop  4411  ideqg  4412  elrnmpt  4508  elrnmpt1  4510  elrnmptg  4511  cnveqb  4701  relcoi1  4774  funopg  4858  funcnvuni  4892  fun11iun  5070  fvelrnb  5144  fvmptg  5171  fndmin  5197  eldmrexrn  5231  foelrn  5240  foco2  5241  fmptco  5253  elabrex  5320  abrexco  5321  f1veqaeq  5331  f1oiso  5388  eusvobj2  5420  acexmidlema  5425  acexmidlemb  5426  acexmidlem2  5431  acexmidlemv  5432  oprabid  5459  mpt2fun  5524  elrnmpt2g  5534  elrnmpt2  5535  ralrnmpt2  5536  rexrnmpt2  5537  ovi3  5558  ov6g  5559  ovelrn  5570  caovcang  5583  caovcan  5586  eloprabi  5743  dftpos4  5798  elqsg  6065  qsel  6092  brecop  6105  eroveu  6106  erovlem  6107  th3qlem1  6117  th3q  6120  nqtri3or  6253  enq0sym  6285  enq0ref  6286  enq0tr  6287  enq0breq  6289  addnq0mo  6300  mulnq0mo  6301  mulnnnq0  6303  genipv  6361  genpelvl  6364  genpelvu  6365  addsrmo  6488  mulsrmo  6489  ltresr  6548  axcnre  6571  bj-nn0suc0  6851  bj-inf2vnlem1  6867  bj-inf2vnlem2  6868  bj-nn0sucALT  6875