Theorem eqeq1 2172

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1341   = wceq 1343   ∈ wcel 2136

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqeq1i  2173  eqeq1d  2174  eqeq2  2175  eqeq12  2178  eqtr  2183  eqsb1lem  2269  clelab  2292  neeq1  2349  pm13.18  2417  issetf  2733  sbhypf  2775  vtoclgft  2776  eqvincf  2851  pm13.183  2864  eueq  2897  mob  2908  euind  2913  reuind  2931  eqsbc1  2990  csbhypf  3083  uniiunlem  3231  snjust  3581  elsng  3591  elprg  3596  rabrsndc  3644  sneqrg  3742  preq12bg  3753  intab  3853  dfiin2g  3899  exmidsssnc  4182  opthg  4216  copsexg  4222  euotd  4232  elopab  4236  snnex  4426  uniuni  4429  eusv1  4430  reusv3  4438  ordtriexmid  4498  ontriexmidim  4499  onsucelsucexmidlem1  4505  onsucelsucexmid  4507  regexmidlemm  4509  regexmidlem1  4510  reg2exmidlema  4511  wetriext  4554  nn0suc  4581  nndceq0  4595  0elnn  4596  elxpi  4620  opbrop  4683  relop  4754  ideqg  4755  elrnmpt  4853  elrnmpt1  4855  elrnmptg  4856  cnveqb  5059  relcoi1  5135  funopg  5222  funcnvuni  5257  f0rn0  5382  fun11iun  5453  fvelrnb  5534  fvmptg  5562  fndmin  5592  eldmrexrn  5626  fmptco  5651  foco2  5722  elabrex  5726  abrexco  5727  f1veqaeq  5737  f1oiso  5794  eusvobj2  5828  acexmidlema  5833  acexmidlemb  5834  acexmidlem2  5839  acexmidlemv  5840  oprabid  5874  mpofun  5944  elrnmpog  5954  elrnmpo  5955  ralrnmpo  5956  rexrnmpo  5957  ovi3  5978  ov6g  5979  ovelrn  5990  caovcang  6003  caovcan  6006  eloprabi  6164  dftpos4  6231  tfr1onlemaccex  6316  tfrcllemaccex  6329  elqsg  6551  qsel  6578  brecop  6591  eroveu  6592  erovlem  6593  th3qlem1  6603  th3q  6606  elixpsn  6701  ixpsnf1o  6702  2dom  6771  fundmen  6772  xpf1o  6810  nneneq  6823  tridc  6865  fisseneq  6897  fidcenumlemrks  6918  elfi  6936  supsnti  6970  isotilem  6971  updjudhcoinrg  7046  updjud  7047  omp1eom  7060  difinfsn  7065  ctmlemr  7073  ismkvnex  7119  omniwomnimkv  7131  exmidaclem  7164  exmidac  7165  onntri35  7193  indpi  7283  nqtri3or  7337  enq0sym  7373  enq0ref  7374  enq0tr  7375  enq0breq  7377  addnq0mo  7388  mulnq0mo  7389  mulnnnq0  7391  genipv  7450  genpelvl  7453  genpelvu  7454  addsrmo  7684  mulsrmo  7685  aptisr  7720  ltresr  7780  axcnre  7822  axpre-apti  7826  ltordlem  8380  apreap  8485  apreim  8501  aprcl  8544  sup3exmid  8852  creur  8854  creui  8855  nn1m1nn  8875  nn1gt1  8891  elz  9193  nn0ind-raph  9308  nltpnft  9750  xnegeq  9763  xrpnfdc  9778  xrmnfdc  9779  xleaddadd  9823  flqeqceilz  10253  1tonninf  10375  iseqf1olemqval  10422  iseqf1olemqk  10429  seq3f1olemqsum  10435  exp3val  10457  shftfvalg  10760  shftfval  10763  summodc  11324  fsum3  11328  telfsumo  11407  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodmodc  11519  fprodseq  11524  fprodcl2lem  11546  ndvdssub  11867  gcdval  11892  bezoutlemnewy  11929  bezoutlema  11932  bezoutlemb  11933  lcmval  11995  coprmgcdb  12020  coprmdvds1  12023  divgcdcoprmex  12034  dvdsprime  12054  nprm  12055  dvdsprm  12069  coprm  12076  qnumval  12117  qdenval  12118  m1dvdsndvds  12180  reumodprminv  12185  pceu  12227  pcval  12228  pczpre  12229  pcdiv  12234  4sqlem2  12319  4sqlem4  12322  ennnfonelemj0  12334  ennnfonelemjn  12335  ennnfonelem0  12338  ennnfonelemp1  12339  ennnfonelemnn0  12355  ennnfonelemim  12357  unct  12375  istopon  12651  toponsspwpwg  12660  epttop  12730  txuni2  12896  xmeteq0  12999  comet  13139  lgsval  13545  lgsfvalg  13546  lgsval2lem  13551  2sqlem2  13591  2sqlem8  13599  2sqlem9  13600  bj-charfunbi  13693  bj-nn0suc0  13832  bj-inf2vnlem1  13852  bj-inf2vnlem2  13853  bj-nn0sucALT  13860  exmid1stab  13880  subctctexmid  13881  pw1nct  13883  nnsf  13885  peano3nninf  13887  nninfall  13889  exmidsbthr  13902  trilpo  13922  trirec0  13923  redcwlpo  13934  redc0  13936  dceqnconst  13938