Theorem eqeq1 2238

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqeq1i  2239  eqeq1d  2240  eqeq2  2241  eqeq12  2244  eqtr  2249  eqsb1lem  2334  clelab  2358  neeq1  2416  pm13.18  2484  issetf  2811  sbhypf  2854  vtoclgft  2855  eqvincf  2932  pm13.183  2945  eueq  2978  mob  2989  euind  2994  reuind  3012  eqsbc1  3072  csbhypf  3167  uniiunlem  3318  snjust  3678  elsng  3688  elprg  3693  rabrsndc  3743  sneqrg  3850  preq12bg  3861  intab  3962  dfiin2g  4008  exmidsssnc  4299  exmid1stab  4304  opthg  4336  copsexg  4342  euotd  4353  elopab  4358  snnex  4551  uniuni  4554  eusv1  4555  reusv3  4563  ordtriexmid  4625  ontriexmidim  4626  onsucelsucexmidlem1  4632  onsucelsucexmid  4634  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  wetriext  4681  nn0suc  4708  nndceq0  4722  0elnn  4723  elxpi  4747  opbrop  4811  relop  4886  ideqg  4887  elrnmpt  4987  elrnmpt1  4989  elrnmptg  4990  restidsing  5075  cnveqb  5199  relcoi1  5275  funopg  5367  funcnvuni  5406  f0rn0  5540  fun11iun  5613  fvelrnb  5702  fvmptg  5731  fndmin  5763  eldmrexrn  5796  fmptco  5821  foco2  5904  elabrex  5908  elabrexg  5909  abrexco  5910  f1veqaeq  5920  f1oiso  5977  eusvobj2  6014  acexmidlema  6019  acexmidlemb  6020  acexmidlem2  6025  acexmidlemv  6026  oprabid  6060  mpofun  6133  elrnmpog  6144  elrnmpo  6145  ralrnmpo  6146  rexrnmpo  6147  ovi3  6169  ov6g  6170  ovelrn  6181  caovcang  6194  caovcan  6197  eloprabi  6370  funsssuppss  6436  suppssrst  6439  suppssrgst  6440  dftpos4  6472  tfr1onlemaccex  6557  tfrcllemaccex  6570  elqsg  6797  qsel  6824  brecop  6837  eroveu  6838  erovlem  6839  th3qlem1  6849  th3q  6852  elixpsn  6947  ixpsnf1o  6948  2dom  7023  fundmen  7024  xpf1o  7073  nneneq  7086  tridc  7132  elssdc  7137  eqsndc  7138  prfidceq  7163  tpfidceq  7165  fisseneq  7170  fidcenumlemrks  7195  elfi  7213  supsnti  7247  isotilem  7248  updjudhcoinrg  7323  updjud  7324  omp1eom  7337  difinfsn  7342  ctmlemr  7350  ismkvnex  7397  omniwomnimkv  7409  nninfwlpoimlemginf  7418  nninfwlpoimlemdc  7419  nninfinfwlpolem  7420  exmidaclem  7466  exmidac  7467  onntri35  7498  exmidapne  7522  indpi  7605  nqtri3or  7659  enq0sym  7695  enq0ref  7696  enq0tr  7697  enq0breq  7699  addnq0mo  7710  mulnq0mo  7711  mulnnnq0  7713  genipv  7772  genpelvl  7775  genpelvu  7776  addsrmo  8006  mulsrmo  8007  aptisr  8042  ltresr  8102  axcnre  8144  axpre-apti  8148  ltordlem  8704  apreap  8809  apreim  8825  aprcl  8868  aptap  8872  sup3exmid  9179  creur  9181  creui  9182  nn1m1nn  9203  nn1gt1  9219  elz  9525  nn0ind-raph  9641  nltpnft  10093  xnegeq  10106  xrpnfdc  10121  xrmnfdc  10122  xleaddadd  10166  flqeqceilz  10626  1tonninf  10749  iseqf1olemqval  10808  iseqf1olemqk  10815  seq3f1olemqsum  10821  exp3val  10849  wrd2ind  11353  shftfvalg  11441  shftfval  11444  summodc  12007  fsum3  12011  telfsumo  12090  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodmodc  12202  fprodseq  12207  fprodcl2lem  12229  ndvdssub  12554  gcdval  12593  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  lcmval  12698  coprmgcdb  12723  coprmdvds1  12726  divgcdcoprmex  12737  dvdsprime  12757  nprm  12758  dvdsprm  12772  coprm  12779  qnumval  12820  qdenval  12821  m1dvdsndvds  12884  reumodprminv  12889  pceu  12931  pcval  12932  pczpre  12933  pcdiv  12938  4sqlem2  13025  4sqlem4  13028  4sqlemafi  13031  4sqexercise1  13034  4sqexercise2  13035  4sqlemsdc  13036  4sqlem12  13038  4sq  13046  ennnfonelemj0  13085  ennnfonelemjn  13086  ennnfonelem0  13089  ennnfonelemp1  13090  ennnfonelemnn0  13106  ennnfonelemim  13108  unct  13126  gsum0g  13542  gsumval2  13543  ghmf1  13923  rrgeq0i  14342  domneq0  14351  lss1d  14462  lspsn  14495  ellspsn  14496  znf1o  14730  znidom  14736  znunit  14738  istopon  14807  toponsspwpwg  14816  epttop  14884  txuni2  15050  xmeteq0  15153  comet  15293  elply  15528  elply2  15529  mpodvdsmulf1o  15787  perfectlem2  15797  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  gausslemma2dlem0i  15859  2lgslem1b  15891  2lgslem3  15903  2sqlem2  15917  2sqlem8  15925  2sqlem9  15926  upgredg2vtx  16072  uspgredg2v  16145  ushgredgedgloop  16152  vtxduspgrfvedgfi  16225  1loopgrvd2fi  16229  wlkeq  16278  depindlem1  16430  bj-charfunbi  16510  bj-nn0suc0  16649  bj-inf2vnlem1  16669  bj-inf2vnlem2  16670  bj-nn0sucALT  16677  subctctexmid  16705  pw1nct  16708  exmidnotnotr  16710  exmidcon  16711  exmidpeirce  16712  nnsf  16714  peano3nninf  16716  nninfall  16718  exmidsbthr  16734  trilpo  16758  trirec0  16759  redcwlpo  16771  redc0  16773  dceqnconst  16776  gfsumval  16792