Theorem eqeq1 2200

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqeq1i  2201  eqeq1d  2202  eqeq2  2203  eqeq12  2206  eqtr  2211  eqsb1lem  2296  clelab  2319  neeq1  2377  pm13.18  2445  issetf  2767  sbhypf  2809  vtoclgft  2810  eqvincf  2885  pm13.183  2898  eueq  2931  mob  2942  euind  2947  reuind  2965  eqsbc1  3025  csbhypf  3119  uniiunlem  3268  snjust  3623  elsng  3633  elprg  3638  rabrsndc  3686  sneqrg  3788  preq12bg  3799  intab  3899  dfiin2g  3945  exmidsssnc  4232  exmid1stab  4237  opthg  4267  copsexg  4273  euotd  4283  elopab  4288  snnex  4479  uniuni  4482  eusv1  4483  reusv3  4491  ordtriexmid  4553  ontriexmidim  4554  onsucelsucexmidlem1  4560  onsucelsucexmid  4562  regexmidlemm  4564  regexmidlem1  4565  reg2exmidlema  4566  wetriext  4609  nn0suc  4636  nndceq0  4650  0elnn  4651  elxpi  4675  opbrop  4738  relop  4812  ideqg  4813  elrnmpt  4911  elrnmpt1  4913  elrnmptg  4914  restidsing  4998  cnveqb  5121  relcoi1  5197  funopg  5288  funcnvuni  5323  f0rn0  5448  fun11iun  5521  fvelrnb  5604  fvmptg  5633  fndmin  5665  eldmrexrn  5699  fmptco  5724  foco2  5796  elabrex  5800  elabrexg  5801  abrexco  5802  f1veqaeq  5812  f1oiso  5869  eusvobj2  5904  acexmidlema  5909  acexmidlemb  5910  acexmidlem2  5915  acexmidlemv  5916  oprabid  5950  mpofun  6020  elrnmpog  6031  elrnmpo  6032  ralrnmpo  6033  rexrnmpo  6034  ovi3  6055  ov6g  6056  ovelrn  6067  caovcang  6080  caovcan  6083  eloprabi  6249  dftpos4  6316  tfr1onlemaccex  6401  tfrcllemaccex  6414  elqsg  6639  qsel  6666  brecop  6679  eroveu  6680  erovlem  6681  th3qlem1  6691  th3q  6694  elixpsn  6789  ixpsnf1o  6790  2dom  6859  fundmen  6860  xpf1o  6900  nneneq  6913  tridc  6955  fisseneq  6988  fidcenumlemrks  7012  elfi  7030  supsnti  7064  isotilem  7065  updjudhcoinrg  7140  updjud  7141  omp1eom  7154  difinfsn  7159  ctmlemr  7167  ismkvnex  7214  omniwomnimkv  7226  nninfwlpoimlemginf  7235  nninfwlpoimlemdc  7236  exmidaclem  7268  exmidac  7269  onntri35  7297  exmidapne  7320  indpi  7402  nqtri3or  7456  enq0sym  7492  enq0ref  7493  enq0tr  7494  enq0breq  7496  addnq0mo  7507  mulnq0mo  7508  mulnnnq0  7510  genipv  7569  genpelvl  7572  genpelvu  7573  addsrmo  7803  mulsrmo  7804  aptisr  7839  ltresr  7899  axcnre  7941  axpre-apti  7945  ltordlem  8501  apreap  8606  apreim  8622  aprcl  8665  aptap  8669  sup3exmid  8976  creur  8978  creui  8979  nn1m1nn  9000  nn1gt1  9016  elz  9319  nn0ind-raph  9434  nltpnft  9880  xnegeq  9893  xrpnfdc  9908  xrmnfdc  9909  xleaddadd  9953  flqeqceilz  10389  1tonninf  10512  iseqf1olemqval  10571  iseqf1olemqk  10578  seq3f1olemqsum  10584  exp3val  10612  shftfvalg  10962  shftfval  10965  summodc  11526  fsum3  11530  telfsumo  11609  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodmodc  11721  fprodseq  11726  fprodcl2lem  11748  ndvdssub  12071  gcdval  12096  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  lcmval  12201  coprmgcdb  12226  coprmdvds1  12229  divgcdcoprmex  12240  dvdsprime  12260  nprm  12261  dvdsprm  12275  coprm  12282  qnumval  12323  qdenval  12324  m1dvdsndvds  12386  reumodprminv  12391  pceu  12433  pcval  12434  pczpre  12435  pcdiv  12440  4sqlem2  12527  4sqlem4  12530  4sqlemafi  12533  4sqexercise1  12536  4sqexercise2  12537  4sqlemsdc  12538  4sqlem12  12540  4sq  12548  ennnfonelemj0  12558  ennnfonelemjn  12559  ennnfonelem0  12562  ennnfonelemp1  12563  ennnfonelemnn0  12579  ennnfonelemim  12581  unct  12599  gsum0g  12979  gsumval2  12980  ghmf1  13343  rrgeq0i  13760  domneq0  13768  lss1d  13879  lspsn  13912  ellspsn  13913  znf1o  14139  znidom  14145  znunit  14147  istopon  14181  toponsspwpwg  14190  epttop  14258  txuni2  14424  xmeteq0  14527  comet  14667  elply  14880  elply2  14881  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  gausslemma2dlem0i  15173  2sqlem2  15202  2sqlem8  15210  2sqlem9  15211  bj-charfunbi  15303  bj-nn0suc0  15442  bj-inf2vnlem1  15462  bj-inf2vnlem2  15463  bj-nn0sucALT  15470  subctctexmid  15491  pw1nct  15493  nnsf  15495  peano3nninf  15497  nninfall  15499  exmidsbthr  15513  trilpo  15533  trirec0  15534  redcwlpo  15545  redc0  15547  dceqnconst  15550