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 1606	. . . 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 1395   = wceq 1397   ∈ 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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  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  2357  neeq1  2415  pm13.18  2483  issetf  2810  sbhypf  2853  vtoclgft  2854  eqvincf  2931  pm13.183  2944  eueq  2977  mob  2988  euind  2993  reuind  3011  eqsbc1  3071  csbhypf  3166  uniiunlem  3316  snjust  3674  elsng  3684  elprg  3689  rabrsndc  3739  sneqrg  3845  preq12bg  3856  intab  3957  dfiin2g  4003  exmidsssnc  4293  exmid1stab  4298  opthg  4330  copsexg  4336  euotd  4347  elopab  4352  snnex  4545  uniuni  4548  eusv1  4549  reusv3  4557  ordtriexmid  4619  ontriexmidim  4620  onsucelsucexmidlem1  4626  onsucelsucexmid  4628  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  wetriext  4675  nn0suc  4702  nndceq0  4716  0elnn  4717  elxpi  4741  opbrop  4805  relop  4880  ideqg  4881  elrnmpt  4981  elrnmpt1  4983  elrnmptg  4984  restidsing  5069  cnveqb  5192  relcoi1  5268  funopg  5360  funcnvuni  5399  f0rn0  5531  fun11iun  5604  fvelrnb  5693  fvmptg  5722  fndmin  5754  eldmrexrn  5788  fmptco  5813  foco2  5894  elabrex  5898  elabrexg  5899  abrexco  5900  f1veqaeq  5910  f1oiso  5967  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlem2  6015  acexmidlemv  6016  oprabid  6050  mpofun  6123  elrnmpog  6134  elrnmpo  6135  ralrnmpo  6136  rexrnmpo  6137  ovi3  6159  ov6g  6160  ovelrn  6171  caovcang  6184  caovcan  6187  eloprabi  6361  dftpos4  6429  tfr1onlemaccex  6514  tfrcllemaccex  6527  elqsg  6754  qsel  6781  brecop  6794  eroveu  6795  erovlem  6796  th3qlem1  6806  th3q  6809  elixpsn  6904  ixpsnf1o  6905  2dom  6980  fundmen  6981  xpf1o  7030  nneneq  7043  tridc  7089  elssdc  7094  eqsndc  7095  prfidceq  7120  tpfidceq  7122  fisseneq  7127  fidcenumlemrks  7152  elfi  7170  supsnti  7204  isotilem  7205  updjudhcoinrg  7280  updjud  7281  omp1eom  7294  difinfsn  7299  ctmlemr  7307  ismkvnex  7354  omniwomnimkv  7366  nninfwlpoimlemginf  7375  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  exmidaclem  7423  exmidac  7424  onntri35  7455  exmidapne  7479  indpi  7562  nqtri3or  7616  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  addnq0mo  7667  mulnq0mo  7668  mulnnnq0  7670  genipv  7729  genpelvl  7732  genpelvu  7733  addsrmo  7963  mulsrmo  7964  aptisr  7999  ltresr  8059  axcnre  8101  axpre-apti  8105  ltordlem  8662  apreap  8767  apreim  8783  aprcl  8826  aptap  8830  sup3exmid  9137  creur  9139  creui  9140  nn1m1nn  9161  nn1gt1  9177  elz  9481  nn0ind-raph  9597  nltpnft  10049  xnegeq  10062  xrpnfdc  10077  xrmnfdc  10078  xleaddadd  10122  flqeqceilz  10581  1tonninf  10704  iseqf1olemqval  10763  iseqf1olemqk  10770  seq3f1olemqsum  10776  exp3val  10804  wrd2ind  11308  shftfvalg  11383  shftfval  11386  summodc  11949  fsum3  11953  telfsumo  12032  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodmodc  12144  fprodseq  12149  fprodcl2lem  12171  ndvdssub  12496  gcdval  12535  bezoutlemnewy  12572  bezoutlema  12575  bezoutlemb  12576  lcmval  12640  coprmgcdb  12665  coprmdvds1  12668  divgcdcoprmex  12679  dvdsprime  12699  nprm  12700  dvdsprm  12714  coprm  12721  qnumval  12762  qdenval  12763  m1dvdsndvds  12826  reumodprminv  12831  pceu  12873  pcval  12874  pczpre  12875  pcdiv  12880  4sqlem2  12967  4sqlem4  12970  4sqlemafi  12973  4sqexercise1  12976  4sqexercise2  12977  4sqlemsdc  12978  4sqlem12  12980  4sq  12988  ennnfonelemj0  13027  ennnfonelemjn  13028  ennnfonelem0  13031  ennnfonelemp1  13032  ennnfonelemnn0  13048  ennnfonelemim  13050  unct  13068  gsum0g  13484  gsumval2  13485  ghmf1  13865  rrgeq0i  14284  domneq0  14292  lss1d  14403  lspsn  14436  ellspsn  14437  znf1o  14671  znidom  14677  znunit  14679  istopon  14743  toponsspwpwg  14752  epttop  14820  txuni2  14986  xmeteq0  15089  comet  15229  elply  15464  elply2  15465  mpodvdsmulf1o  15720  perfectlem2  15730  lgsval  15739  lgsfvalg  15740  lgsval2lem  15745  gausslemma2dlem0i  15792  2lgslem1b  15824  2lgslem3  15836  2sqlem2  15850  2sqlem8  15858  2sqlem9  15859  upgredg2vtx  16005  uspgredg2v  16078  ushgredgedgloop  16085  vtxduspgrfvedgfi  16158  1loopgrvd2fi  16162  wlkeq  16211  depindlem1  16351  bj-charfunbi  16432  bj-nn0suc0  16571  bj-inf2vnlem1  16591  bj-inf2vnlem2  16592  bj-nn0sucALT  16599  subctctexmid  16627  pw1nct  16630  nnsf  16633  peano3nninf  16635  nninfall  16637  exmidsbthr  16653  trilpo  16673  trirec0  16674  redcwlpo  16686  redc0  16688  dceqnconst  16691  gfsumval  16707