Theorem eqeq1 2239

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

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

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 2214

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

This theorem is referenced by:  eqeq1i  2240  eqeq1d  2241  eqeq2  2242  eqeq12  2245  eqtr  2250  eqsb1lem  2335  clelab  2360  neeq1  2425  pm13.18  2493  issetf  2821  sbhypf  2864  vtoclgft  2865  eqvincf  2942  pm13.183  2955  eueq  2988  mob  2999  euind  3004  reuind  3022  eqsbc1  3082  csbhypf  3177  uniiunlem  3328  snjust  3694  elsng  3704  elprg  3709  rabrsndc  3759  sneqrg  3866  preq12bg  3877  intab  3978  dfiin2g  4024  exmidsssnc  4316  exmid1stab  4321  opthg  4354  copsexg  4360  euotd  4371  elopab  4376  snnex  4569  uniuni  4572  eusv1  4573  reusv3  4581  ordtriexmid  4643  ontriexmidim  4644  onsucelsucexmidlem1  4650  onsucelsucexmid  4652  regexmidlemm  4654  regexmidlem1  4655  reg2exmidlema  4656  wetriext  4699  nn0suc  4726  nndceq0  4740  0elnn  4741  elxpi  4765  opbrop  4829  relop  4905  ideqg  4906  elrnmpt  5006  elrnmpt1  5008  elrnmptg  5009  restidsing  5094  cnveqb  5218  relcoi1  5294  funopg  5386  funcnvuni  5425  f0rn0  5562  fun11iun  5635  fvelrnb  5724  fvmptg  5753  fndmin  5785  eldmrexrn  5818  fmptco  5843  foco2  5926  elabrex  5930  elabrexg  5931  abrexco  5932  f1veqaeq  5942  f1oiso  5999  eusvobj2  6036  acexmidlema  6041  acexmidlemb  6042  acexmidlem2  6047  acexmidlemv  6048  oprabid  6082  mpofun  6155  elrnmpog  6166  elrnmpo  6167  ralrnmpo  6168  rexrnmpo  6169  ovi3  6191  ov6g  6192  ovelrn  6203  caovcang  6216  caovcan  6219  eloprabi  6392  funsssuppss  6458  suppssrst  6461  suppssrgst  6462  dftpos4  6494  tfr1onlemaccex  6579  tfrcllemaccex  6592  elqsg  6819  qsel  6846  brecop  6859  eroveu  6860  erovlem  6861  th3qlem1  6871  th3q  6874  elixpsn  6970  ixpsnf1o  6971  2dom  7046  fundmen  7047  xpf1o  7097  nneneq  7111  tridc  7157  elssdc  7162  eqsndc  7163  prfidceq  7188  tpfidceq  7190  fisseneq  7195  fidcenumlemrks  7223  elfi  7258  supsnti  7296  isotilem  7297  updjudhcoinrg  7372  updjud  7373  omp1eom  7386  difinfsn  7391  ctmlemr  7399  ismkvnex  7446  omniwomnimkv  7458  nninfwlpoimlemginf  7467  nninfwlpoimlemdc  7468  nninfinfwlpolem  7469  exmidaclem  7515  exmidac  7516  onntri35  7547  exmidapne  7574  indpi  7657  nqtri3or  7711  enq0sym  7747  enq0ref  7748  enq0tr  7749  enq0breq  7751  addnq0mo  7762  mulnq0mo  7763  mulnnnq0  7765  genipv  7824  genpelvl  7827  genpelvu  7828  addsrmo  8058  mulsrmo  8059  aptisr  8094  ltresr  8154  axcnre  8196  axpre-apti  8200  ltordlem  8756  apreap  8861  apreim  8877  aprcl  8920  aptap  8924  sup3exmid  9231  creur  9233  creui  9234  nn1m1nn  9255  nn1gt1  9271  elz  9579  nn0ind-raph  9695  nltpnft  10147  xnegeq  10160  xrpnfdc  10175  xrmnfdc  10176  xleaddadd  10220  flqeqceilz  10680  1tonninf  10803  iseqf1olemqval  10862  iseqf1olemqk  10869  seq3f1olemqsum  10875  exp3val  10903  wrd2ind  11415  shftfvalg  11503  shftfval  11506  summodc  12069  fsum3  12073  telfsumo  12152  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodmodc  12264  fprodseq  12269  fprodcl2lem  12291  ndvdssub  12616  gcdval  12655  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  lcmval  12760  coprmgcdb  12785  coprmdvds1  12788  divgcdcoprmex  12799  dvdsprime  12819  nprm  12820  dvdsprm  12834  coprm  12841  qnumval  12882  qdenval  12883  m1dvdsndvds  12946  reumodprminv  12951  pceu  12993  pcval  12994  pczpre  12995  pcdiv  13000  4sqlem2  13087  4sqlem4  13090  4sqlemafi  13093  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  4sqlem12  13100  4sq  13108  ballotfilem2  13142  ennnfonelemj0  13152  ennnfonelemjn  13153  ennnfonelem0  13156  ennnfonelemp1  13157  ennnfonelemnn0  13173  ennnfonelemim  13175  unct  13193  gsum0g  13609  gsumval2  13610  ghmf1  13990  rrgeq0i  14409  domneq0  14418  lss1d  14531  lspsn  14564  ellspsn  14565  znf1o  14799  znidom  14805  znunit  14807  istopon  14878  toponsspwpwg  14887  epttop  14955  txuni2  15121  xmeteq0  15224  comet  15364  elply  15599  elply2  15600  mpodvdsmulf1o  15858  perfectlem2  15868  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  gausslemma2dlem0i  15930  2lgslem1b  15962  2lgslem3  15974  2sqlem2  15988  2sqlem8  15996  2sqlem9  15997  upgredg2vtx  16143  uspgredg2v  16216  ushgredgedgloop  16223  vtxduspgrfvedgfi  16296  1loopgrvd2fi  16300  wlkeq  16349  depindlem1  16501  bj-charfunbi  16581  bj-nn0suc0  16720  bj-inf2vnlem1  16740  bj-inf2vnlem2  16741  bj-nn0sucALT  16748  subctctexmid  16774  pw1nct  16777  exmidnotnotr  16779  exmidcon  16780  exmidpeirce  16781  nnsf  16783  peano3nninf  16785  nninfall  16787  exmidsbthr  16803  trilpo  16827  trirec0  16828  redcwlpo  16840  redc0  16842  dceqnconst  16846  gfsumval  16862