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  suppinisegdc  6513  dftpos4  6539  tfr1onlemaccex  6624  tfrcllemaccex  6637  elqsg  6864  qsel  6891  brecop  6904  eroveu  6905  erovlem  6906  th3qlem1  6916  th3q  6919  elixpsn  7023  ixpsnf1o  7024  2dom  7099  fundmen  7100  xpf1o  7150  nneneq  7164  tridc  7210  elssdc  7215  eqsndc  7216  prfidceq  7241  tpfidceq  7243  fisseneq  7248  fidcenumlemrks  7277  funisfsuppdc  7298  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  9655  nn0ind-raph  9773  nltpnft  10232  xnegeq  10245  xrpnfdc  10260  xrmnfdc  10261  xleaddadd  10305  flqeqceilz  10775  1tonninf  10898  iseqf1olemqval  10957  iseqf1olemqk  10964  seq3f1olemqsum  10970  exp3val  10998  wrd2ind  11516  shftfvalg  11604  shftfval  11607  summodc  12174  fsum3  12178  telfsumo  12257  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodmodc  12369  fprodseq  12374  fprodcl2lem  12396  ndvdssub  12721  gcdval  12760  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  lcmval  12865  coprmgcdb  12890  coprmdvds1  12893  divgcdcoprmex  12904  dvdsprime  12924  nprm  12925  dvdsprm  12940  coprm  12947  qnumval  12989  qdenval  12990  m1dvdsndvds  13055  reumodprminv  13060  pceu  13102  pcval  13103  pczpre  13104  pcdiv  13109  4sqlem2  13196  4sqlem4  13199  4sqlemafi  13202  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  4sqlem12  13209  4sq  13217  ballotfilem2  13285  ennnfonelemj0  13349  ennnfonelemjn  13350  ennnfonelem0  13353  ennnfonelemp1  13354  ennnfonelemnn0  13370  ennnfonelemim  13372  unct  13390  gzsum0  13771  gzsumval2  13772  ghmf1  14134  gsumvalfi  14241  rrgeq0i  14680  domneq0  14689  lss1d  14828  lspsn  14861  ellspsn  14862  znf1o  15094  znidom  15100  znunit  15102  psrlidmfi  15208  psrridmfi  15209  mvrval2  15216  mvrf1fi  15219  istopon  15256  toponsspwpwg  15265  epttop  15333  txuni2  15499  xmeteq0  15602  comet  15742  elply  15977  elply2  15978  mpodvdsmulf1o  16301  perfectlem2  16317  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  gausslemma2dlem0i  16398  2lgslem1b  16430  2lgslem3  16442  2sqlem2  16456  2sqlem8  16464  2sqlem9  16465  upgredg2vtx  16611  uspgredg2v  16684  ushgredgedgloop  16691  vtxduspgrfvedgfi  16764  1loopgrvd2fi  16768  wlkeq  16817  depindlem1  16969  bj-charfunbi  17059  bj-nn0suc0  17198  bj-inf2vnlem1  17218  bj-inf2vnlem2  17219  bj-nn0sucALT  17226  subctctexmid  17252  pw1nct  17255  exmidnotnotr  17258  exmidcon  17259  exmidpeirce  17260  stnot  17261  wexmiddc  17264  idjudju  17269  nnsf  17271  peano3nninf  17273  nninfall  17275  exmidsbthr  17291  trilpo  17316  trirec0  17317  redcwlpo  17329  redc0  17331  dceqnconst  17334