Theorem eqeq1 2087

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

Assertion

Ref	Expression
eqeq1	⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2075	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 118	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1490	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 231	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1745	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2075	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2075	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 221	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 103  ∀wal 1282   = wceq 1284   ∈ wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqeq1i  2088  eqeq1d  2089  eqeq2  2090  eqeq12  2093  eqtr  2098  eqsb3lem  2181  clelab  2203  neeq1  2258  pm13.18  2326  issetf  2606  sbhypf  2648  vtoclgft  2649  eqvincf  2720  pm13.183  2732  eueq  2763  mob  2774  euind  2779  reuind  2795  eqsbc3  2853  csbhypf  2941  uniiunlem  3082  snjust  3403  elsng  3413  elprg  3418  rabrsndc  3460  sneqrg  3554  preq12bg  3565  intab  3665  dfiin2g  3711  opthg  3993  copsexg  3999  euotd  4009  elopab  4013  snnex  4199  uniuni  4201  eusv1  4202  reusv3  4210  ordtriexmid  4265  onsucelsucexmidlem1  4271  onsucelsucexmid  4273  regexmidlemm  4275  regexmidlem1  4276  reg2exmidlema  4277  wetriext  4319  nn0suc  4345  nndceq0  4357  0elnn  4358  elxpi  4379  opbrop  4437  relop  4504  ideqg  4505  elrnmpt  4601  elrnmpt1  4603  elrnmptg  4604  cnveqb  4796  relcoi1  4869  funopg  4954  funcnvuni  4988  fun11iun  5167  fvelrnb  5242  fvmptg  5269  fndmin  5295  eldmrexrn  5329  foelrn  5338  foco2  5339  fmptco  5351  elabrex  5418  abrexco  5419  f1veqaeq  5429  f1oiso  5485  eusvobj2  5518  acexmidlema  5523  acexmidlemb  5524  acexmidlem2  5529  acexmidlemv  5530  oprabid  5557  mpt2fun  5623  elrnmpt2g  5633  elrnmpt2  5634  ralrnmpt2  5635  rexrnmpt2  5636  ovi3  5657  ov6g  5658  ovelrn  5669  caovcang  5682  caovcan  5685  eloprabi  5842  dftpos4  5901  elqsg  6179  qsel  6206  brecop  6219  eroveu  6220  erovlem  6221  th3qlem1  6231  th3q  6234  2dom  6308  fundmen  6309  nneneq  6343  supsnti  6418  isotilem  6419  indpi  6532  nqtri3or  6586  enq0sym  6622  enq0ref  6623  enq0tr  6624  enq0breq  6626  addnq0mo  6637  mulnq0mo  6638  mulnnnq0  6640  genipv  6699  genpelvl  6702  genpelvu  6703  addsrmo  6920  mulsrmo  6921  aptisr  6955  ltresr  7007  axcnre  7047  axpre-apti  7051  apreap  7687  apreim  7703  creur  8036  creui  8037  nn1m1nn  8057  nn1gt1  8072  elz  8353  nn0ind-raph  8464  nltpnft  8884  xnegeq  8894  flqeqceilz  9320  expival  9478  shftfvalg  9706  shftfval  9709  ndvdssub  10330  gcdval  10351  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  lcmval  10445  coprmgcdb  10470  coprmdvds1  10473  divgcdcoprmex  10484  dvdsprime  10504  nprm  10505  dvdsprm  10518  coprm  10523  bj-nn0suc0  10745  bj-inf2vnlem1  10765  bj-inf2vnlem2  10766  bj-nn0sucALT  10773