Theorem eqeq1 2203

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeq1i  2204  eqeq1d  2205  eqeq2  2206  eqeq12  2209  eqtr  2214  eqsb1lem  2299  clelab  2322  neeq1  2380  pm13.18  2448  issetf  2770  sbhypf  2813  vtoclgft  2814  eqvincf  2889  pm13.183  2902  eueq  2935  mob  2946  euind  2951  reuind  2969  eqsbc1  3029  csbhypf  3123  uniiunlem  3273  snjust  3628  elsng  3638  elprg  3643  rabrsndc  3691  sneqrg  3793  preq12bg  3804  intab  3904  dfiin2g  3950  exmidsssnc  4237  exmid1stab  4242  opthg  4272  copsexg  4278  euotd  4288  elopab  4293  snnex  4484  uniuni  4487  eusv1  4488  reusv3  4496  ordtriexmid  4558  ontriexmidim  4559  onsucelsucexmidlem1  4565  onsucelsucexmid  4567  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  wetriext  4614  nn0suc  4641  nndceq0  4655  0elnn  4656  elxpi  4680  opbrop  4743  relop  4817  ideqg  4818  elrnmpt  4916  elrnmpt1  4918  elrnmptg  4919  restidsing  5003  cnveqb  5126  relcoi1  5202  funopg  5293  funcnvuni  5328  f0rn0  5455  fun11iun  5528  fvelrnb  5611  fvmptg  5640  fndmin  5672  eldmrexrn  5706  fmptco  5731  foco2  5803  elabrex  5807  elabrexg  5808  abrexco  5809  f1veqaeq  5819  f1oiso  5876  eusvobj2  5911  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  acexmidlemv  5923  oprabid  5957  mpofun  6028  elrnmpog  6039  elrnmpo  6040  ralrnmpo  6041  rexrnmpo  6042  ovi3  6064  ov6g  6065  ovelrn  6076  caovcang  6089  caovcan  6092  eloprabi  6263  dftpos4  6330  tfr1onlemaccex  6415  tfrcllemaccex  6428  elqsg  6653  qsel  6680  brecop  6693  eroveu  6694  erovlem  6695  th3qlem1  6705  th3q  6708  elixpsn  6803  ixpsnf1o  6804  2dom  6873  fundmen  6874  xpf1o  6914  nneneq  6927  tridc  6969  prfidceq  6998  tpfidceq  7000  fisseneq  7004  fidcenumlemrks  7028  elfi  7046  supsnti  7080  isotilem  7081  updjudhcoinrg  7156  updjud  7157  omp1eom  7170  difinfsn  7175  ctmlemr  7183  ismkvnex  7230  omniwomnimkv  7242  nninfwlpoimlemginf  7251  nninfwlpoimlemdc  7252  nninfinfwlpolem  7253  exmidaclem  7293  exmidac  7294  onntri35  7322  exmidapne  7345  indpi  7428  nqtri3or  7482  enq0sym  7518  enq0ref  7519  enq0tr  7520  enq0breq  7522  addnq0mo  7533  mulnq0mo  7534  mulnnnq0  7536  genipv  7595  genpelvl  7598  genpelvu  7599  addsrmo  7829  mulsrmo  7830  aptisr  7865  ltresr  7925  axcnre  7967  axpre-apti  7971  ltordlem  8528  apreap  8633  apreim  8649  aprcl  8692  aptap  8696  sup3exmid  9003  creur  9005  creui  9006  nn1m1nn  9027  nn1gt1  9043  elz  9347  nn0ind-raph  9462  nltpnft  9908  xnegeq  9921  xrpnfdc  9936  xrmnfdc  9937  xleaddadd  9981  flqeqceilz  10429  1tonninf  10552  iseqf1olemqval  10611  iseqf1olemqk  10618  seq3f1olemqsum  10624  exp3val  10652  shftfvalg  11002  shftfval  11005  summodc  11567  fsum3  11571  telfsumo  11650  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodmodc  11762  fprodseq  11767  fprodcl2lem  11789  ndvdssub  12114  gcdval  12153  bezoutlemnewy  12190  bezoutlema  12193  bezoutlemb  12194  lcmval  12258  coprmgcdb  12283  coprmdvds1  12286  divgcdcoprmex  12297  dvdsprime  12317  nprm  12318  dvdsprm  12332  coprm  12339  qnumval  12380  qdenval  12381  m1dvdsndvds  12444  reumodprminv  12449  pceu  12491  pcval  12492  pczpre  12493  pcdiv  12498  4sqlem2  12585  4sqlem4  12588  4sqlemafi  12591  4sqexercise1  12594  4sqexercise2  12595  4sqlemsdc  12596  4sqlem12  12598  4sq  12606  ennnfonelemj0  12645  ennnfonelemjn  12646  ennnfonelem0  12649  ennnfonelemp1  12650  ennnfonelemnn0  12666  ennnfonelemim  12668  unct  12686  gsum0g  13100  gsumval2  13101  ghmf1  13481  rrgeq0i  13898  domneq0  13906  lss1d  14017  lspsn  14050  ellspsn  14051  znf1o  14285  znidom  14291  znunit  14293  istopon  14357  toponsspwpwg  14366  epttop  14434  txuni2  14600  xmeteq0  14703  comet  14843  elply  15078  elply2  15079  mpodvdsmulf1o  15334  perfectlem2  15344  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  gausslemma2dlem0i  15406  2lgslem1b  15438  2lgslem3  15450  2sqlem2  15464  2sqlem8  15472  2sqlem9  15473  bj-charfunbi  15565  bj-nn0suc0  15704  bj-inf2vnlem1  15724  bj-inf2vnlem2  15725  bj-nn0sucALT  15732  subctctexmid  15755  pw1nct  15758  nnsf  15760  peano3nninf  15762  nninfall  15764  exmidsbthr  15780  trilpo  15800  trirec0  15801  redcwlpo  15812  redc0  15814  dceqnconst  15817