Theorem eqeq1 2211

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1370   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  eqeq1i  2212  eqeq1d  2213  eqeq2  2214  eqeq12  2217  eqtr  2222  eqsb1lem  2307  clelab  2330  neeq1  2388  pm13.18  2456  issetf  2778  sbhypf  2821  vtoclgft  2822  eqvincf  2897  pm13.183  2910  eueq  2943  mob  2954  euind  2959  reuind  2977  eqsbc1  3037  csbhypf  3131  uniiunlem  3281  snjust  3637  elsng  3647  elprg  3652  rabrsndc  3700  sneqrg  3802  preq12bg  3813  intab  3913  dfiin2g  3959  exmidsssnc  4246  exmid1stab  4251  opthg  4281  copsexg  4287  euotd  4298  elopab  4303  snnex  4494  uniuni  4497  eusv1  4498  reusv3  4506  ordtriexmid  4568  ontriexmidim  4569  onsucelsucexmidlem1  4575  onsucelsucexmid  4577  regexmidlemm  4579  regexmidlem1  4580  reg2exmidlema  4581  wetriext  4624  nn0suc  4651  nndceq0  4665  0elnn  4666  elxpi  4690  opbrop  4753  relop  4827  ideqg  4828  elrnmpt  4926  elrnmpt1  4928  elrnmptg  4929  restidsing  5014  cnveqb  5137  relcoi1  5213  funopg  5304  funcnvuni  5342  f0rn0  5469  fun11iun  5542  fvelrnb  5625  fvmptg  5654  fndmin  5686  eldmrexrn  5720  fmptco  5745  foco2  5821  elabrex  5825  elabrexg  5826  abrexco  5827  f1veqaeq  5837  f1oiso  5894  eusvobj2  5929  acexmidlema  5934  acexmidlemb  5935  acexmidlem2  5940  acexmidlemv  5941  oprabid  5975  mpofun  6046  elrnmpog  6057  elrnmpo  6058  ralrnmpo  6059  rexrnmpo  6060  ovi3  6082  ov6g  6083  ovelrn  6094  caovcang  6107  caovcan  6110  eloprabi  6281  dftpos4  6348  tfr1onlemaccex  6433  tfrcllemaccex  6446  elqsg  6671  qsel  6698  brecop  6711  eroveu  6712  erovlem  6713  th3qlem1  6723  th3q  6726  elixpsn  6821  ixpsnf1o  6822  2dom  6896  fundmen  6897  xpf1o  6940  nneneq  6953  tridc  6995  prfidceq  7024  tpfidceq  7026  fisseneq  7030  fidcenumlemrks  7054  elfi  7072  supsnti  7106  isotilem  7107  updjudhcoinrg  7182  updjud  7183  omp1eom  7196  difinfsn  7201  ctmlemr  7209  ismkvnex  7256  omniwomnimkv  7268  nninfwlpoimlemginf  7277  nninfwlpoimlemdc  7278  nninfinfwlpolem  7279  exmidaclem  7319  exmidac  7320  onntri35  7348  exmidapne  7371  indpi  7454  nqtri3or  7508  enq0sym  7544  enq0ref  7545  enq0tr  7546  enq0breq  7548  addnq0mo  7559  mulnq0mo  7560  mulnnnq0  7562  genipv  7621  genpelvl  7624  genpelvu  7625  addsrmo  7855  mulsrmo  7856  aptisr  7891  ltresr  7951  axcnre  7993  axpre-apti  7997  ltordlem  8554  apreap  8659  apreim  8675  aprcl  8718  aptap  8722  sup3exmid  9029  creur  9031  creui  9032  nn1m1nn  9053  nn1gt1  9069  elz  9373  nn0ind-raph  9489  nltpnft  9935  xnegeq  9948  xrpnfdc  9963  xrmnfdc  9964  xleaddadd  10008  flqeqceilz  10461  1tonninf  10584  iseqf1olemqval  10643  iseqf1olemqk  10650  seq3f1olemqsum  10656  exp3val  10684  shftfvalg  11071  shftfval  11074  summodc  11636  fsum3  11640  telfsumo  11719  mertenslemub  11787  mertenslemi1  11788  mertenslem2  11789  mertensabs  11790  prodmodc  11831  fprodseq  11836  fprodcl2lem  11858  ndvdssub  12183  gcdval  12222  bezoutlemnewy  12259  bezoutlema  12262  bezoutlemb  12263  lcmval  12327  coprmgcdb  12352  coprmdvds1  12355  divgcdcoprmex  12366  dvdsprime  12386  nprm  12387  dvdsprm  12401  coprm  12408  qnumval  12449  qdenval  12450  m1dvdsndvds  12513  reumodprminv  12518  pceu  12560  pcval  12561  pczpre  12562  pcdiv  12567  4sqlem2  12654  4sqlem4  12657  4sqlemafi  12660  4sqexercise1  12663  4sqexercise2  12664  4sqlemsdc  12665  4sqlem12  12667  4sq  12675  ennnfonelemj0  12714  ennnfonelemjn  12715  ennnfonelem0  12718  ennnfonelemp1  12719  ennnfonelemnn0  12735  ennnfonelemim  12737  unct  12755  gsum0g  13170  gsumval2  13171  ghmf1  13551  rrgeq0i  13968  domneq0  13976  lss1d  14087  lspsn  14120  ellspsn  14121  znf1o  14355  znidom  14361  znunit  14363  istopon  14427  toponsspwpwg  14436  epttop  14504  txuni2  14670  xmeteq0  14773  comet  14913  elply  15148  elply2  15149  mpodvdsmulf1o  15404  perfectlem2  15414  lgsval  15423  lgsfvalg  15424  lgsval2lem  15429  gausslemma2dlem0i  15476  2lgslem1b  15508  2lgslem3  15520  2sqlem2  15534  2sqlem8  15542  2sqlem9  15543  bj-charfunbi  15680  bj-nn0suc0  15819  bj-inf2vnlem1  15839  bj-inf2vnlem2  15840  bj-nn0sucALT  15847  subctctexmid  15870  pw1nct  15873  nnsf  15875  peano3nninf  15877  nninfall  15879  exmidsbthr  15895  trilpo  15915  trirec0  15916  redcwlpo  15927  redc0  15929  dceqnconst  15932