Theorem eqeq1 2184

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqeq1i  2185  eqeq1d  2186  eqeq2  2187  eqeq12  2190  eqtr  2195  eqsb1lem  2280  clelab  2303  neeq1  2360  pm13.18  2428  issetf  2744  sbhypf  2786  vtoclgft  2787  eqvincf  2862  pm13.183  2875  eueq  2908  mob  2919  euind  2924  reuind  2942  eqsbc1  3002  csbhypf  3095  uniiunlem  3244  snjust  3597  elsng  3607  elprg  3612  rabrsndc  3660  sneqrg  3762  preq12bg  3773  intab  3873  dfiin2g  3919  exmidsssnc  4203  exmid1stab  4208  opthg  4238  copsexg  4244  euotd  4254  elopab  4258  snnex  4448  uniuni  4451  eusv1  4452  reusv3  4460  ordtriexmid  4520  ontriexmidim  4521  onsucelsucexmidlem1  4527  onsucelsucexmid  4529  regexmidlemm  4531  regexmidlem1  4532  reg2exmidlema  4533  wetriext  4576  nn0suc  4603  nndceq0  4617  0elnn  4618  elxpi  4642  opbrop  4705  relop  4777  ideqg  4778  elrnmpt  4876  elrnmpt1  4878  elrnmptg  4879  restidsing  4963  cnveqb  5084  relcoi1  5160  funopg  5250  funcnvuni  5285  f0rn0  5410  fun11iun  5482  fvelrnb  5563  fvmptg  5592  fndmin  5623  eldmrexrn  5657  fmptco  5682  foco2  5754  elabrex  5758  abrexco  5759  f1veqaeq  5769  f1oiso  5826  eusvobj2  5860  acexmidlema  5865  acexmidlemb  5866  acexmidlem2  5871  acexmidlemv  5872  oprabid  5906  mpofun  5976  elrnmpog  5986  elrnmpo  5987  ralrnmpo  5988  rexrnmpo  5989  ovi3  6010  ov6g  6011  ovelrn  6022  caovcang  6035  caovcan  6038  eloprabi  6196  dftpos4  6263  tfr1onlemaccex  6348  tfrcllemaccex  6361  elqsg  6584  qsel  6611  brecop  6624  eroveu  6625  erovlem  6626  th3qlem1  6636  th3q  6639  elixpsn  6734  ixpsnf1o  6735  2dom  6804  fundmen  6805  xpf1o  6843  nneneq  6856  tridc  6898  fisseneq  6930  fidcenumlemrks  6951  elfi  6969  supsnti  7003  isotilem  7004  updjudhcoinrg  7079  updjud  7080  omp1eom  7093  difinfsn  7098  ctmlemr  7106  ismkvnex  7152  omniwomnimkv  7164  nninfwlpoimlemginf  7173  nninfwlpoimlemdc  7174  exmidaclem  7206  exmidac  7207  onntri35  7235  exmidapne  7258  indpi  7340  nqtri3or  7394  enq0sym  7430  enq0ref  7431  enq0tr  7432  enq0breq  7434  addnq0mo  7445  mulnq0mo  7446  mulnnnq0  7448  genipv  7507  genpelvl  7510  genpelvu  7511  addsrmo  7741  mulsrmo  7742  aptisr  7777  ltresr  7837  axcnre  7879  axpre-apti  7883  ltordlem  8438  apreap  8543  apreim  8559  aprcl  8602  aptap  8606  sup3exmid  8913  creur  8915  creui  8916  nn1m1nn  8936  nn1gt1  8952  elz  9254  nn0ind-raph  9369  nltpnft  9813  xnegeq  9826  xrpnfdc  9841  xrmnfdc  9842  xleaddadd  9886  flqeqceilz  10317  1tonninf  10439  iseqf1olemqval  10486  iseqf1olemqk  10493  seq3f1olemqsum  10499  exp3val  10521  shftfvalg  10826  shftfval  10829  summodc  11390  fsum3  11394  telfsumo  11473  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodmodc  11585  fprodseq  11590  fprodcl2lem  11612  ndvdssub  11934  gcdval  11959  bezoutlemnewy  11996  bezoutlema  11999  bezoutlemb  12000  lcmval  12062  coprmgcdb  12087  coprmdvds1  12090  divgcdcoprmex  12101  dvdsprime  12121  nprm  12122  dvdsprm  12136  coprm  12143  qnumval  12184  qdenval  12185  m1dvdsndvds  12247  reumodprminv  12252  pceu  12294  pcval  12295  pczpre  12296  pcdiv  12301  4sqlem2  12386  4sqlem4  12389  ennnfonelemj0  12401  ennnfonelemjn  12402  ennnfonelem0  12405  ennnfonelemp1  12406  ennnfonelemnn0  12422  ennnfonelemim  12424  unct  12442  istopon  13483  toponsspwpwg  13492  epttop  13560  txuni2  13726  xmeteq0  13829  comet  13969  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  2sqlem2  14432  2sqlem8  14440  2sqlem9  14441  bj-charfunbi  14533  bj-nn0suc0  14672  bj-inf2vnlem1  14692  bj-inf2vnlem2  14693  bj-nn0sucALT  14700  subctctexmid  14720  pw1nct  14722  nnsf  14724  peano3nninf  14726  nninfall  14728  exmidsbthr  14741  trilpo  14761  trirec0  14762  redcwlpo  14773  redc0  14775  dceqnconst  14777