Theorem eqeq1 2203

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeq1i  2204  eqeq1d  2205  eqeq2  2206  eqeq12  2209  eqtr  2214  eqsb1lem  2299  clelab  2322  neeq1  2380  pm13.18  2448  issetf  2770  sbhypf  2813  vtoclgft  2814  eqvincf  2889  pm13.183  2902  eueq  2935  mob  2946  euind  2951  reuind  2969  eqsbc1  3029  csbhypf  3123  uniiunlem  3273  snjust  3628  elsng  3638  elprg  3643  rabrsndc  3691  sneqrg  3793  preq12bg  3804  intab  3904  dfiin2g  3950  exmidsssnc  4237  exmid1stab  4242  opthg  4272  copsexg  4278  euotd  4288  elopab  4293  snnex  4484  uniuni  4487  eusv1  4488  reusv3  4496  ordtriexmid  4558  ontriexmidim  4559  onsucelsucexmidlem1  4565  onsucelsucexmid  4567  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  wetriext  4614  nn0suc  4641  nndceq0  4655  0elnn  4656  elxpi  4680  opbrop  4743  relop  4817  ideqg  4818  elrnmpt  4916  elrnmpt1  4918  elrnmptg  4919  restidsing  5003  cnveqb  5126  relcoi1  5202  funopg  5293  funcnvuni  5328  f0rn0  5455  fun11iun  5528  fvelrnb  5611  fvmptg  5640  fndmin  5672  eldmrexrn  5706  fmptco  5731  foco2  5803  elabrex  5807  elabrexg  5808  abrexco  5809  f1veqaeq  5819  f1oiso  5876  eusvobj2  5911  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  acexmidlemv  5923  oprabid  5957  mpofun  6028  elrnmpog  6039  elrnmpo  6040  ralrnmpo  6041  rexrnmpo  6042  ovi3  6064  ov6g  6065  ovelrn  6076  caovcang  6089  caovcan  6092  eloprabi  6263  dftpos4  6330  tfr1onlemaccex  6415  tfrcllemaccex  6428  elqsg  6653  qsel  6680  brecop  6693  eroveu  6694  erovlem  6695  th3qlem1  6705  th3q  6708  elixpsn  6803  ixpsnf1o  6804  2dom  6873  fundmen  6874  xpf1o  6914  nneneq  6927  tridc  6969  prfidceq  6998  tpfidceq  7000  fisseneq  7004  fidcenumlemrks  7028  elfi  7046  supsnti  7080  isotilem  7081  updjudhcoinrg  7156  updjud  7157  omp1eom  7170  difinfsn  7175  ctmlemr  7183  ismkvnex  7230  omniwomnimkv  7242  nninfwlpoimlemginf  7251  nninfwlpoimlemdc  7252  exmidaclem  7291  exmidac  7292  onntri35  7320  exmidapne  7343  indpi  7426  nqtri3or  7480  enq0sym  7516  enq0ref  7517  enq0tr  7518  enq0breq  7520  addnq0mo  7531  mulnq0mo  7532  mulnnnq0  7534  genipv  7593  genpelvl  7596  genpelvu  7597  addsrmo  7827  mulsrmo  7828  aptisr  7863  ltresr  7923  axcnre  7965  axpre-apti  7969  ltordlem  8526  apreap  8631  apreim  8647  aprcl  8690  aptap  8694  sup3exmid  9001  creur  9003  creui  9004  nn1m1nn  9025  nn1gt1  9041  elz  9345  nn0ind-raph  9460  nltpnft  9906  xnegeq  9919  xrpnfdc  9934  xrmnfdc  9935  xleaddadd  9979  flqeqceilz  10427  1tonninf  10550  iseqf1olemqval  10609  iseqf1olemqk  10616  seq3f1olemqsum  10622  exp3val  10650  shftfvalg  11000  shftfval  11003  summodc  11565  fsum3  11569  telfsumo  11648  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodmodc  11760  fprodseq  11765  fprodcl2lem  11787  ndvdssub  12112  gcdval  12151  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  lcmval  12256  coprmgcdb  12281  coprmdvds1  12284  divgcdcoprmex  12295  dvdsprime  12315  nprm  12316  dvdsprm  12330  coprm  12337  qnumval  12378  qdenval  12379  m1dvdsndvds  12442  reumodprminv  12447  pceu  12489  pcval  12490  pczpre  12491  pcdiv  12496  4sqlem2  12583  4sqlem4  12586  4sqlemafi  12589  4sqexercise1  12592  4sqexercise2  12593  4sqlemsdc  12594  4sqlem12  12596  4sq  12604  ennnfonelemj0  12643  ennnfonelemjn  12644  ennnfonelem0  12647  ennnfonelemp1  12648  ennnfonelemnn0  12664  ennnfonelemim  12666  unct  12684  gsum0g  13098  gsumval2  13099  ghmf1  13479  rrgeq0i  13896  domneq0  13904  lss1d  14015  lspsn  14048  ellspsn  14049  znf1o  14283  znidom  14289  znunit  14291  istopon  14333  toponsspwpwg  14342  epttop  14410  txuni2  14576  xmeteq0  14679  comet  14819  elply  15054  elply2  15055  mpodvdsmulf1o  15310  perfectlem2  15320  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  gausslemma2dlem0i  15382  2lgslem1b  15414  2lgslem3  15426  2sqlem2  15440  2sqlem8  15448  2sqlem9  15449  bj-charfunbi  15541  bj-nn0suc0  15680  bj-inf2vnlem1  15700  bj-inf2vnlem2  15701  bj-nn0sucALT  15708  subctctexmid  15731  pw1nct  15734  nnsf  15736  peano3nninf  15738  nninfall  15740  exmidsbthr  15754  trilpo  15774  trirec0  15775  redcwlpo  15786  redc0  15788  dceqnconst  15791