Theorem eqeq1 2177

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 2164	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 119	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1551	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 232	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1817	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2164	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2164	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1346   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqeq1i  2178  eqeq1d  2179  eqeq2  2180  eqeq12  2183  eqtr  2188  eqsb1lem  2273  clelab  2296  neeq1  2353  pm13.18  2421  issetf  2737  sbhypf  2779  vtoclgft  2780  eqvincf  2855  pm13.183  2868  eueq  2901  mob  2912  euind  2917  reuind  2935  eqsbc1  2994  csbhypf  3087  uniiunlem  3236  snjust  3588  elsng  3598  elprg  3603  rabrsndc  3651  sneqrg  3749  preq12bg  3760  intab  3860  dfiin2g  3906  exmidsssnc  4189  opthg  4223  copsexg  4229  euotd  4239  elopab  4243  snnex  4433  uniuni  4436  eusv1  4437  reusv3  4445  ordtriexmid  4505  ontriexmidim  4506  onsucelsucexmidlem1  4512  onsucelsucexmid  4514  regexmidlemm  4516  regexmidlem1  4517  reg2exmidlema  4518  wetriext  4561  nn0suc  4588  nndceq0  4602  0elnn  4603  elxpi  4627  opbrop  4690  relop  4761  ideqg  4762  elrnmpt  4860  elrnmpt1  4862  elrnmptg  4863  cnveqb  5066  relcoi1  5142  funopg  5232  funcnvuni  5267  f0rn0  5392  fun11iun  5463  fvelrnb  5544  fvmptg  5572  fndmin  5603  eldmrexrn  5637  fmptco  5662  foco2  5733  elabrex  5737  abrexco  5738  f1veqaeq  5748  f1oiso  5805  eusvobj2  5839  acexmidlema  5844  acexmidlemb  5845  acexmidlem2  5850  acexmidlemv  5851  oprabid  5885  mpofun  5955  elrnmpog  5965  elrnmpo  5966  ralrnmpo  5967  rexrnmpo  5968  ovi3  5989  ov6g  5990  ovelrn  6001  caovcang  6014  caovcan  6017  eloprabi  6175  dftpos4  6242  tfr1onlemaccex  6327  tfrcllemaccex  6340  elqsg  6563  qsel  6590  brecop  6603  eroveu  6604  erovlem  6605  th3qlem1  6615  th3q  6618  elixpsn  6713  ixpsnf1o  6714  2dom  6783  fundmen  6784  xpf1o  6822  nneneq  6835  tridc  6877  fisseneq  6909  fidcenumlemrks  6930  elfi  6948  supsnti  6982  isotilem  6983  updjudhcoinrg  7058  updjud  7059  omp1eom  7072  difinfsn  7077  ctmlemr  7085  ismkvnex  7131  omniwomnimkv  7143  nninfwlpoimlemginf  7152  nninfwlpoimlemdc  7153  exmidaclem  7185  exmidac  7186  onntri35  7214  indpi  7304  nqtri3or  7358  enq0sym  7394  enq0ref  7395  enq0tr  7396  enq0breq  7398  addnq0mo  7409  mulnq0mo  7410  mulnnnq0  7412  genipv  7471  genpelvl  7474  genpelvu  7475  addsrmo  7705  mulsrmo  7706  aptisr  7741  ltresr  7801  axcnre  7843  axpre-apti  7847  ltordlem  8401  apreap  8506  apreim  8522  aprcl  8565  sup3exmid  8873  creur  8875  creui  8876  nn1m1nn  8896  nn1gt1  8912  elz  9214  nn0ind-raph  9329  nltpnft  9771  xnegeq  9784  xrpnfdc  9799  xrmnfdc  9800  xleaddadd  9844  flqeqceilz  10274  1tonninf  10396  iseqf1olemqval  10443  iseqf1olemqk  10450  seq3f1olemqsum  10456  exp3val  10478  shftfvalg  10782  shftfval  10785  summodc  11346  fsum3  11350  telfsumo  11429  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodmodc  11541  fprodseq  11546  fprodcl2lem  11568  ndvdssub  11889  gcdval  11914  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  lcmval  12017  coprmgcdb  12042  coprmdvds1  12045  divgcdcoprmex  12056  dvdsprime  12076  nprm  12077  dvdsprm  12091  coprm  12098  qnumval  12139  qdenval  12140  m1dvdsndvds  12202  reumodprminv  12207  pceu  12249  pcval  12250  pczpre  12251  pcdiv  12256  4sqlem2  12341  4sqlem4  12344  ennnfonelemj0  12356  ennnfonelemjn  12357  ennnfonelem0  12360  ennnfonelemp1  12361  ennnfonelemnn0  12377  ennnfonelemim  12379  unct  12397  istopon  12805  toponsspwpwg  12814  epttop  12884  txuni2  13050  xmeteq0  13153  comet  13293  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  2sqlem2  13745  2sqlem8  13753  2sqlem9  13754  bj-charfunbi  13846  bj-nn0suc0  13985  bj-inf2vnlem1  14005  bj-inf2vnlem2  14006  bj-nn0sucALT  14013  exmid1stab  14033  subctctexmid  14034  pw1nct  14036  nnsf  14038  peano3nninf  14040  nninfall  14042  exmidsbthr  14055  trilpo  14075  trirec0  14076  redcwlpo  14087  redc0  14089  dceqnconst  14091