Theorem eqeq1 2238

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 2225	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1606	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 233	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1872	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2225	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2225	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1395   = wceq 1397   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqeq1i  2239  eqeq1d  2240  eqeq2  2241  eqeq12  2244  eqtr  2249  eqsb1lem  2334  clelab  2357  neeq1  2415  pm13.18  2483  issetf  2810  sbhypf  2853  vtoclgft  2854  eqvincf  2931  pm13.183  2944  eueq  2977  mob  2988  euind  2993  reuind  3011  eqsbc1  3071  csbhypf  3166  uniiunlem  3316  snjust  3674  elsng  3684  elprg  3689  rabrsndc  3739  sneqrg  3845  preq12bg  3856  intab  3957  dfiin2g  4003  exmidsssnc  4293  exmid1stab  4298  opthg  4330  copsexg  4336  euotd  4347  elopab  4352  snnex  4545  uniuni  4548  eusv1  4549  reusv3  4557  ordtriexmid  4619  ontriexmidim  4620  onsucelsucexmidlem1  4626  onsucelsucexmid  4628  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  wetriext  4675  nn0suc  4702  nndceq0  4716  0elnn  4717  elxpi  4741  opbrop  4805  relop  4880  ideqg  4881  elrnmpt  4981  elrnmpt1  4983  elrnmptg  4984  restidsing  5069  cnveqb  5192  relcoi1  5268  funopg  5360  funcnvuni  5399  f0rn0  5531  fun11iun  5604  fvelrnb  5693  fvmptg  5722  fndmin  5754  eldmrexrn  5788  fmptco  5813  foco2  5893  elabrex  5897  elabrexg  5898  abrexco  5899  f1veqaeq  5909  f1oiso  5966  eusvobj2  6003  acexmidlema  6008  acexmidlemb  6009  acexmidlem2  6014  acexmidlemv  6015  oprabid  6049  mpofun  6122  elrnmpog  6133  elrnmpo  6134  ralrnmpo  6135  rexrnmpo  6136  ovi3  6158  ov6g  6159  ovelrn  6170  caovcang  6183  caovcan  6186  eloprabi  6360  dftpos4  6428  tfr1onlemaccex  6513  tfrcllemaccex  6526  elqsg  6753  qsel  6780  brecop  6793  eroveu  6794  erovlem  6795  th3qlem1  6805  th3q  6808  elixpsn  6903  ixpsnf1o  6904  2dom  6979  fundmen  6980  xpf1o  7029  nneneq  7042  tridc  7088  elssdc  7093  eqsndc  7094  prfidceq  7119  tpfidceq  7121  fisseneq  7126  fidcenumlemrks  7151  elfi  7169  supsnti  7203  isotilem  7204  updjudhcoinrg  7279  updjud  7280  omp1eom  7293  difinfsn  7298  ctmlemr  7306  ismkvnex  7353  omniwomnimkv  7365  nninfwlpoimlemginf  7374  nninfwlpoimlemdc  7375  nninfinfwlpolem  7376  exmidaclem  7422  exmidac  7423  onntri35  7454  exmidapne  7478  indpi  7561  nqtri3or  7615  enq0sym  7651  enq0ref  7652  enq0tr  7653  enq0breq  7655  addnq0mo  7666  mulnq0mo  7667  mulnnnq0  7669  genipv  7728  genpelvl  7731  genpelvu  7732  addsrmo  7962  mulsrmo  7963  aptisr  7998  ltresr  8058  axcnre  8100  axpre-apti  8104  ltordlem  8661  apreap  8766  apreim  8782  aprcl  8825  aptap  8829  sup3exmid  9136  creur  9138  creui  9139  nn1m1nn  9160  nn1gt1  9176  elz  9480  nn0ind-raph  9596  nltpnft  10048  xnegeq  10061  xrpnfdc  10076  xrmnfdc  10077  xleaddadd  10121  flqeqceilz  10579  1tonninf  10702  iseqf1olemqval  10761  iseqf1olemqk  10768  seq3f1olemqsum  10774  exp3val  10802  wrd2ind  11303  shftfvalg  11378  shftfval  11381  summodc  11943  fsum3  11947  telfsumo  12026  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodmodc  12138  fprodseq  12143  fprodcl2lem  12165  ndvdssub  12490  gcdval  12529  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  lcmval  12634  coprmgcdb  12659  coprmdvds1  12662  divgcdcoprmex  12673  dvdsprime  12693  nprm  12694  dvdsprm  12708  coprm  12715  qnumval  12756  qdenval  12757  m1dvdsndvds  12820  reumodprminv  12825  pceu  12867  pcval  12868  pczpre  12869  pcdiv  12874  4sqlem2  12961  4sqlem4  12964  4sqlemafi  12967  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  4sqlem12  12974  4sq  12982  ennnfonelemj0  13021  ennnfonelemjn  13022  ennnfonelem0  13025  ennnfonelemp1  13026  ennnfonelemnn0  13042  ennnfonelemim  13044  unct  13062  gsum0g  13478  gsumval2  13479  ghmf1  13859  rrgeq0i  14277  domneq0  14285  lss1d  14396  lspsn  14429  ellspsn  14430  znf1o  14664  znidom  14670  znunit  14672  istopon  14736  toponsspwpwg  14745  epttop  14813  txuni2  14979  xmeteq0  15082  comet  15222  elply  15457  elply2  15458  mpodvdsmulf1o  15713  perfectlem2  15723  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  gausslemma2dlem0i  15785  2lgslem1b  15817  2lgslem3  15829  2sqlem2  15843  2sqlem8  15851  2sqlem9  15852  upgredg2vtx  15998  uspgredg2v  16071  ushgredgedgloop  16078  vtxduspgrfvedgfi  16151  1loopgrvd2fi  16155  wlkeq  16204  bj-charfunbi  16406  bj-nn0suc0  16545  bj-inf2vnlem1  16565  bj-inf2vnlem2  16566  bj-nn0sucALT  16573  subctctexmid  16601  pw1nct  16604  nnsf  16607  peano3nninf  16609  nninfall  16611  exmidsbthr  16627  trilpo  16647  trirec0  16648  redcwlpo  16659  redc0  16661  dceqnconst  16664  gfsumval  16680