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  4340  exmid1stab  4345  opthg  4378  copsexg  4384  euotd  4395  elopab  4400  snnex  4594  uniuni  4597  eusv1  4598  reusv3  4606  ordtriexmid  4668  ontriexmidim  4669  onsucelsucexmidlem1  4675  onsucelsucexmid  4677  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  wetriext  4724  nn0suc  4751  nndceq0  4765  0elnn  4766  elxpi  4790  opbrop  4854  relop  4930  ideqg  4931  elrnmpt  5031  elrnmpt1  5033  elrnmptg  5034  restidsing  5119  cnveqb  5243  relcoi1  5319  funopg  5411  funcnvuni  5450  f0rn0  5587  fun11iun  5660  fvelrnb  5750  fvmptg  5781  fndmin  5816  eldmrexrn  5849  fmptco  5874  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1veqaeq  5975  f1oiso  6032  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  acexmidlemv  6083  oprabid  6117  mpofun  6190  elrnmpog  6201  elrnmpo  6202  ralrnmpo  6203  rexrnmpo  6204  ovi3  6226  ov6g  6227  ovelrn  6238  caovcang  6251  caovcan  6254  elabreximd  6356  eloprabi  6432  funsssuppss  6498  suppssrst  6501  suppssrgst  6502  dftpos4  6534  tfr1onlemaccex  6619  tfrcllemaccex  6632  elqsg  6859  qsel  6886  brecop  6899  eroveu  6900  erovlem  6901  th3qlem1  6911  th3q  6914  elixpsn  7017  ixpsnf1o  7018  2dom  7093  fundmen  7094  xpf1o  7144  nneneq  7158  tridc  7204  elssdc  7209  eqsndc  7210  prfidceq  7235  tpfidceq  7237  fisseneq  7242  fidcenumlemrks  7270  elfi  7305  supsnti  7346  isotilem  7347  updjudhcoinrg  7422  updjud  7423  omp1eom  7436  difinfsn  7441  ctmlemr  7449  ismkvnex  7496  omniwomnimkv  7508  nninfwlpoimlemginf  7517  nninfwlpoimlemdc  7518  nninfinfwlpolem  7519  exmidaclem  7565  exmidac  7566  onntri35  7597  exmidapne  7627  indpi  7710  nqtri3or  7764  enq0sym  7800  enq0ref  7801  enq0tr  7802  enq0breq  7804  addnq0mo  7815  mulnq0mo  7816  mulnnnq0  7818  genipv  7877  genpelvl  7880  genpelvu  7881  addsrmo  8111  mulsrmo  8112  aptisr  8147  ltresr  8207  axcnre  8249  axpre-apti  8253  ltordlem  8812  apreap  8918  apreim  8934  aprcl  8977  aptap  8981  sup3exmid  9290  creur  9292  creui  9293  nn1m1nn  9325  nn1gt1  9341  elz  9651  nn0ind-raph  9768  nltpnft  10227  xnegeq  10240  xrpnfdc  10255  xrmnfdc  10256  xleaddadd  10300  flqeqceilz  10770  1tonninf  10893  iseqf1olemqval  10952  iseqf1olemqk  10959  seq3f1olemqsum  10965  exp3val  10993  wrd2ind  11511  shftfvalg  11599  shftfval  11602  summodc  12169  fsum3  12173  telfsumo  12252  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodmodc  12364  fprodseq  12369  fprodcl2lem  12391  ndvdssub  12716  gcdval  12755  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  lcmval  12860  coprmgcdb  12885  coprmdvds1  12888  divgcdcoprmex  12899  dvdsprime  12919  nprm  12920  dvdsprm  12935  coprm  12942  qnumval  12984  qdenval  12985  m1dvdsndvds  13050  reumodprminv  13055  pceu  13097  pcval  13098  pczpre  13099  pcdiv  13104  4sqlem2  13191  4sqlem4  13194  4sqlemafi  13197  4sqexercise1  13200  4sqexercise2  13201  4sqlemsdc  13202  4sqlem12  13204  4sq  13212  ballotfilem2  13280  ennnfonelemj0  13344  ennnfonelemjn  13345  ennnfonelem0  13348  ennnfonelemp1  13349  ennnfonelemnn0  13365  ennnfonelemim  13367  unct  13385  gzsum0  13766  gzsumval2  13767  ghmf1  14129  gsumvalfi  14236  rrgeq0i  14656  domneq0  14665  lss1d  14804  lspsn  14837  ellspsn  14838  znf1o  15070  znidom  15076  znunit  15078  istopon  15205  toponsspwpwg  15214  epttop  15282  txuni2  15448  xmeteq0  15551  comet  15691  elply  15926  elply2  15927  mpodvdsmulf1o  16245  perfectlem2  16261  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  gausslemma2dlem0i  16342  2lgslem1b  16374  2lgslem3  16386  2sqlem2  16400  2sqlem8  16408  2sqlem9  16409  upgredg2vtx  16555  uspgredg2v  16628  ushgredgedgloop  16635  vtxduspgrfvedgfi  16708  1loopgrvd2fi  16712  wlkeq  16761  depindlem1  16913  bj-charfunbi  17003  bj-nn0suc0  17142  bj-inf2vnlem1  17162  bj-inf2vnlem2  17163  bj-nn0sucALT  17170  subctctexmid  17196  pw1nct  17199  exmidnotnotr  17202  exmidcon  17203  exmidpeirce  17204  stnot  17205  wexmiddc  17208  nnsf  17214  peano3nninf  17216  nninfall  17218  exmidsbthr  17234  trilpo  17259  trirec0  17260  redcwlpo  17272  redc0  17274  dceqnconst  17277