Theorem eqeq1 2245

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqeq1i  2246  eqeq1d  2247  eqeq2  2248  eqeq12  2251  eqtr  2256  eqsb1lem  2341  clelab  2366  neeq1  2433  pm13.18  2501  issetf  2829  sbhypf  2872  vtoclgft  2873  eqvincf  2951  pm13.183  2964  eueq  2997  mob  3008  euind  3013  reuind  3031  eqsbc1  3091  csbhypf  3186  uniiunlem  3338  snjust  3714  elsng  3724  elprg  3729  rabrsndc  3779  sneqrg  3887  preq12bg  3898  intab  3999  dfiin2g  4045  exmidsssnc  4342  exmid1stab  4347  opthg  4380  copsexg  4386  euotd  4397  elopab  4402  snnex  4596  uniuni  4599  eusv1  4600  reusv3  4608  ordtriexmid  4670  ontriexmidim  4671  onsucelsucexmidlem1  4677  onsucelsucexmid  4679  regexmidlemm  4681  regexmidlem1  4682  reg2exmidlema  4683  wetriext  4726  nn0suc  4753  nndceq0  4767  0elnn  4768  elxpi  4792  opbrop  4856  relop  4932  ideqg  4933  elrnmpt  5033  elrnmpt1  5035  elrnmptg  5036  restidsing  5122  cnveqb  5246  relcoi1  5322  funopg  5414  funcnvuni  5453  f0rn0  5590  fun11iun  5663  fvelrnb  5753  fvmptg  5784  fndmin  5819  eldmrexrn  5852  fmptco  5877  foco2  5962  elabrex  5966  elabrexg  5967  abrexco  5968  f1veqaeq  5978  f1oiso  6035  eusvobj2  6074  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  acexmidlemv  6086  oprabid  6120  mpofun  6193  elrnmpog  6204  elrnmpo  6205  ralrnmpo  6206  rexrnmpo  6207  ovi3  6229  ov6g  6230  ovelrn  6241  caovcang  6254  caovcan  6257  elabreximd  6360  eloprabi  6436  funsssuppss  6502  suppssrst  6505  suppssrgst  6506  dftpos4  6538  tfr1onlemaccex  6623  tfrcllemaccex  6636  elqsg  6863  qsel  6890  brecop  6903  eroveu  6904  erovlem  6905  th3qlem1  6915  th3q  6918  elixpsn  7021  ixpsnf1o  7022  2dom  7097  fundmen  7098  xpf1o  7148  nneneq  7162  tridc  7208  elssdc  7213  eqsndc  7214  prfidceq  7239  tpfidceq  7241  fisseneq  7246  fidcenumlemrks  7275  elfi  7310  supsnti  7351  isotilem  7352  updjudhcoinrg  7427  updjud  7428  omp1eom  7441  difinfsn  7446  ctmlemr  7454  ismkvnex  7501  omniwomnimkv  7513  nninfwlpoimlemginf  7522  nninfwlpoimlemdc  7523  nninfinfwlpolem  7524  exmidaclem  7570  exmidac  7571  onntri35  7602  exmidapne  7632  indpi  7715  nqtri3or  7769  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  mulnnnq0  7823  genipv  7882  genpelvl  7885  genpelvu  7886  addsrmo  8116  mulsrmo  8117  aptisr  8152  ltresr  8212  axcnre  8254  axpre-apti  8258  ltordlem  8817  apreap  8923  apreim  8939  aprcl  8982  aptap  8986  sup3exmid  9295  creur  9297  creui  9298  nn1m1nn  9331  nn1gt1  9347  elz  9657  nn0ind-raph  9774  nltpnft  10233  xnegeq  10246  xrpnfdc  10261  xrmnfdc  10262  xleaddadd  10306  flqeqceilz  10776  1tonninf  10899  iseqf1olemqval  10958  iseqf1olemqk  10965  seq3f1olemqsum  10971  exp3val  10999  wrd2ind  11517  shftfvalg  11605  shftfval  11608  summodc  12175  fsum3  12179  telfsumo  12258  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodmodc  12370  fprodseq  12375  fprodcl2lem  12397  ndvdssub  12722  gcdval  12761  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  lcmval  12866  coprmgcdb  12891  coprmdvds1  12894  divgcdcoprmex  12905  dvdsprime  12925  nprm  12926  dvdsprm  12941  coprm  12948  qnumval  12990  qdenval  12991  m1dvdsndvds  13056  reumodprminv  13061  pceu  13103  pcval  13104  pczpre  13105  pcdiv  13110  4sqlem2  13197  4sqlem4  13200  4sqlemafi  13203  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  4sqlem12  13210  4sq  13218  ballotfilem2  13286  ennnfonelemj0  13350  ennnfonelemjn  13351  ennnfonelem0  13354  ennnfonelemp1  13355  ennnfonelemnn0  13371  ennnfonelemim  13373  unct  13391  gzsum0  13772  gzsumval2  13773  ghmf1  14135  gsumvalfi  14242  rrgeq0i  14681  domneq0  14690  lss1d  14829  lspsn  14862  ellspsn  14863  znf1o  15095  znidom  15101  znunit  15103  psrlidmfi  15199  psrridmfi  15200  istopon  15239  toponsspwpwg  15248  epttop  15316  txuni2  15482  xmeteq0  15585  comet  15725  elply  15960  elply2  15961  mpodvdsmulf1o  16284  perfectlem2  16300  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  gausslemma2dlem0i  16381  2lgslem1b  16413  2lgslem3  16425  2sqlem2  16439  2sqlem8  16447  2sqlem9  16448  upgredg2vtx  16594  uspgredg2v  16667  ushgredgedgloop  16674  vtxduspgrfvedgfi  16747  1loopgrvd2fi  16751  wlkeq  16800  depindlem1  16952  bj-charfunbi  17042  bj-nn0suc0  17181  bj-inf2vnlem1  17201  bj-inf2vnlem2  17202  bj-nn0sucALT  17209  subctctexmid  17235  pw1nct  17238  exmidnotnotr  17241  exmidcon  17242  exmidpeirce  17243  stnot  17244  wexmiddc  17247  idjudju  17252  nnsf  17254  peano3nninf  17256  nninfall  17258  exmidsbthr  17274  trilpo  17299  trirec0  17300  redcwlpo  17312  redc0  17314  dceqnconst  17317