Theorem eqeq1 2029

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 2017	. . . . . 6 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2	1	biimpi 113	. . . . 5 ⊢ (A = B → ∀x(x ∈ A ↔ x ∈ B))
3	2	19.21bi 1434	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
4	3	bibi1d 222	. . 3 ⊢ (A = B → ((x ∈ A ↔ x ∈ 𝐶) ↔ (x ∈ B ↔ x ∈ 𝐶)))
5	4	albidv 1688	. 2 ⊢ (A = B → (∀x(x ∈ A ↔ x ∈ 𝐶) ↔ ∀x(x ∈ B ↔ x ∈ 𝐶)))
6		dfcleq 2017	. 2 ⊢ (A = 𝐶 ↔ ∀x(x ∈ A ↔ x ∈ 𝐶))
7		dfcleq 2017	. 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 1375

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 1382  ax-17 1401  ax-ext 2005

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

This theorem is referenced by:  eqeq1i  2030  eqeq1d  2031  eqeq2  2032  eqeq12  2035  eqtr  2040  eqsb3lem  2123  clelab  2145  neeq1  2196  pm13.18  2263  issetf  2539  sbhypf  2579  vtoclgft  2580  eqvincf  2645  pm13.183  2657  eueq  2688  mob  2699  euind  2704  reuind  2720  eqsbc3  2778  csbhypf  2861  uniiunlem  3004  snjust  3354  elprg  3366  elsncg  3371  rabrsndc  3411  sneqrg  3506  preq12bg  3517  intab  3617  dfiin2g  3663  opthg  3948  copsexg  3954  euotd  3964  elopab  3968  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  5742  dftpos4  5797  elqsg  6061  qsel  6087  brecop  6100  eroveu  6101  erovlem  6102  th3qlem1  6112  th3q  6115  nqtri3or  6246  enq0sym  6273  enq0ref  6274  enq0tr  6275  enq0breq  6277  addnq0mo  6288  mulnq0mo  6289  mulnnnq0  6291  genipv  6344  genpelvl  6346  genpelvu  6347  bj-nn0suc  6523