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  7345  isotilem  7346  updjudhcoinrg  7421  updjud  7422  omp1eom  7435  difinfsn  7440  ctmlemr  7448  ismkvnex  7495  omniwomnimkv  7507  nninfwlpoimlemginf  7516  nninfwlpoimlemdc  7517  nninfinfwlpolem  7518  exmidaclem  7564  exmidac  7565  onntri35  7596  exmidapne  7626  indpi  7709  nqtri3or  7763  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  mulnnnq0  7817  genipv  7876  genpelvl  7879  genpelvu  7880  addsrmo  8110  mulsrmo  8111  aptisr  8146  ltresr  8206  axcnre  8248  axpre-apti  8252  ltordlem  8810  apreap  8915  apreim  8931  aprcl  8974  aptap  8978  sup3exmid  9287  creur  9289  creui  9290  nn1m1nn  9322  nn1gt1  9338  elz  9646  nn0ind-raph  9763  nltpnft  10216  xnegeq  10229  xrpnfdc  10244  xrmnfdc  10245  xleaddadd  10289  flqeqceilz  10755  1tonninf  10878  iseqf1olemqval  10937  iseqf1olemqk  10944  seq3f1olemqsum  10950  exp3val  10978  wrd2ind  11495  shftfvalg  11583  shftfval  11586  summodc  12150  fsum3  12154  telfsumo  12233  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodmodc  12345  fprodseq  12350  fprodcl2lem  12372  ndvdssub  12697  gcdval  12736  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  lcmval  12841  coprmgcdb  12866  coprmdvds1  12869  divgcdcoprmex  12880  dvdsprime  12900  nprm  12901  dvdsprm  12915  coprm  12922  qnumval  12963  qdenval  12964  m1dvdsndvds  13027  reumodprminv  13032  pceu  13074  pcval  13075  pczpre  13076  pcdiv  13081  4sqlem2  13168  4sqlem4  13171  4sqlemafi  13174  4sqexercise1  13177  4sqexercise2  13178  4sqlemsdc  13179  4sqlem12  13181  4sq  13189  ballotfilem2  13228  ennnfonelemj0  13292  ennnfonelemjn  13293  ennnfonelem0  13296  ennnfonelemp1  13297  ennnfonelemnn0  13313  ennnfonelemim  13315  unct  13333  gzsum0  13713  gzsumval2  13714  ghmf1  14076  gsumvalfi  14152  rrgeq0i  14572  domneq0  14581  lss1d  14720  lspsn  14753  ellspsn  14754  znf1o  14986  znidom  14992  znunit  14994  istopon  15114  toponsspwpwg  15123  epttop  15191  txuni2  15357  xmeteq0  15460  comet  15600  elply  15835  elply2  15836  mpodvdsmulf1o  16104  perfectlem2  16114  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  gausslemma2dlem0i  16176  2lgslem1b  16208  2lgslem3  16220  2sqlem2  16234  2sqlem8  16242  2sqlem9  16243  upgredg2vtx  16389  uspgredg2v  16462  ushgredgedgloop  16469  vtxduspgrfvedgfi  16542  1loopgrvd2fi  16546  wlkeq  16595  depindlem1  16747  bj-charfunbi  16837  bj-nn0suc0  16976  bj-inf2vnlem1  16996  bj-inf2vnlem2  16997  bj-nn0sucALT  17004  subctctexmid  17030  pw1nct  17033  exmidnotnotr  17036  exmidcon  17037  exmidpeirce  17038  stnot  17039  wexmiddc  17042  nnsf  17048  peano3nninf  17050  nninfall  17052  exmidsbthr  17068  trilpo  17092  trirec0  17093  redcwlpo  17105  redc0  17107  dceqnconst  17110