Theorem eleq1d 2106

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq1d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq1 2100	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243   ∈ wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  eleq12d  2108  eqeltrd  2114  eqneltrd  2133  eqneltrrd  2134  rspcimdv  2657  rspcimedv  2658  reuind  2744  sbcel2g  2871  sbccsb2g  2879  breq1  3767  breq2  3768  inex1g  3893  intexr  3904  pwex  3932  pwexg  3933  prexgOLD  3946  prexg  3947  opelopabsb  3997  pofun  4049  seex  4072  uniex  4174  uniexg  4175  unexb  4177  reusv3  4192  rabxfrd  4201  onun2  4216  onsucelsucexmid  4255  ordsucunielexmid  4256  tfisi  4310  peano2  4318  seinxp  4411  opabid2  4467  opeliunxp2  4476  elrn2g  4525  opeldm  4538  opeldmg  4540  elreldm  4560  elrn2  4576  opelresg  4619  elsnres  4647  iss  4654  elimasng  4693  issref  4707  rnxpid  4755  unielrel  4845  dffun5r  4914  funopg  4934  brprcneu  5171  tz6.12f  5202  fvelrnb  5221  ssimaex  5234  dmfco  5241  fvmpt3  5251  mptfvex  5256  fvmptf  5263  respreima  5295  fvelrn  5298  ffnfvf  5324  ffvresb  5328  fmptco  5330  fmptcof  5331  fsn  5335  fressnfv  5350  fnex  5383  funfvima  5390  funfvima3  5392  f1mpt  5410  fliftfuns  5438  isoselem  5459  ffnov  5605  fovcl  5606  ovmpt2s  5624  ov2gf  5625  ovg  5639  funimassov  5650  caovclg  5653  elovmpt2  5701  fnofval  5721  off  5724  fnexALT  5740  fornex  5742  f1stres  5786  f2ndres  5787  xp1st  5792  xp2nd  5793  elxp6  5796  unielxp  5800  fmpt2x  5826  mpt2fvex  5829  dftpos4  5878  smoel  5915  tfrlem3-2  5927  tfrlem3-2d  5928  tfrlem8  5934  tfrlem9  5935  tfrlemibxssdm  5941  tfrlemi1  5946  tfrexlem  5948  rdgtfr  5961  rdgon  5973  frecabex  5984  freccl  5993  nnacl  6059  nnmcl  6060  nnmordi  6089  nnaordex  6100  nnm00  6102  erexb  6131  qliftfuns  6190  fundmen  6286  fopwdom  6310  dif1en  6337  diffitest  6344  diffifi  6351  isnumi  6362  addnidpig  6434  indpi  6440  dfplpq2  6452  addclnq  6473  mulclnq  6474  nnnq0lem1  6544  addclnq0  6549  mulclnq0  6550  nqpnq0nq  6551  distrnq0  6557  prloc  6589  prarloclemlo  6592  prarloclem3  6595  prarloclem5  6598  genpml  6615  genpmu  6616  addnqprl  6627  addnqpru  6628  mulnqprl  6666  mulnqpru  6667  ltexprlemell  6696  ltexprlemelu  6697  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  ltexpri  6711  recexprlemm  6722  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  recexpr  6736  addclsr  6838  mulclsr  6839  pitonn  6924  peano2nnnn  6929  axaddrcl  6941  axmulrcl  6943  peano5nnnn  6966  negreb  7276  cju  7913  peano2nn  7926  nn1m1nn  7932  nnaddcl  7934  nnmulcl  7935  nnsub  7952  nndivtr  7955  un0addcl  8215  un0mulcl  8216  elnnnn0  8225  elz  8247  nnnegz  8248  znegclb  8278  zaddcllempos  8282  zaddcllemneg  8284  zaddcl  8285  zmulcl  8297  elz2  8312  zneo  8339  nneoor  8340  zeo  8343  peano5uzti  8346  zindd  8356  uzp1  8506  uzaddcl  8529  ublbneg  8548  eqreznegel  8549  negm  8550  qmulz  8558  qnegcl  8571  irradd  8580  irrmul  8581  fzrev2  8947  negqmod0  9173  frec2uzzd  9186  frec2uzuzd  9188  frecuzrdgrrn  9194  iseqovex  9219  iseqval  9220  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqp1  9225  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqid3  9245  iseqhomo  9248  iseqdistr  9249  expival  9257  expp1  9262  expcllem  9266  expcl2lemap  9267  m1expcl2  9277  shftlem  9417  shftf  9431  cjval  9445  cjth  9446  remim  9460  uzin2  9586  caubnd2  9713  clim  9802  clim2  9804  climshftlemg  9823  climcn1  9829  climcn2  9830  iiserex  9859  climub  9864  climserile  9865  climcau  9866  serif0  9871  bdinex1g  10021  bj-intexr  10028  bj-prexg  10031  bj-uniex  10037  bj-uniexg  10038  bdunexb  10040  bj-indsuc  10052  qdencn  10124