Theorem eleq1d 2226

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 2220	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1335   ∈ wcel 2128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  eleq12d  2228  eqeltrd  2234  eqneltrd  2253  eqneltrrd  2254  rspcimdv  2817  rspcimedv  2818  reuind  2917  sbcel2g  3052  sbccsb2g  3061  breq1  3968  breq2  3969  inex1g  4100  intexr  4111  pwexg  4140  prexg  4170  opelopabsb  4219  pofun  4271  seex  4294  uniex  4396  uniexg  4398  unexb  4400  abnexg  4404  reusv3  4418  rabxfrd  4427  onun2  4447  onsucelsucexmid  4487  ordsucunielexmid  4488  dcextest  4538  tfisi  4544  peano2  4552  seinxp  4654  opabid2  4714  opeliunxp2  4723  elrn2g  4773  opeldm  4786  opeldmg  4788  elreldm  4809  elrn2  4825  opelresg  4870  elsnres  4900  iss  4909  elimasng  4951  issref  4965  rnxpid  5017  unielrel  5110  dffun5r  5179  funopg  5201  brprcneu  5458  tz6.12f  5494  fvelrnb  5513  ssimaex  5526  dmfco  5533  fvmpt3  5544  mptfvex  5550  fvmptf  5557  respreima  5592  fvelrn  5595  ffnfvf  5623  ffvresb  5627  fmptco  5630  fmptcof  5631  fsn  5636  fressnfv  5651  fnex  5686  funfvima  5693  funfvima3  5695  f1mpt  5716  fliftfuns  5743  isoselem  5765  ffnov  5919  fovcl  5920  ovmpos  5938  ov2gf  5939  ovg  5953  funimassov  5964  caovclg  5967  elovmpo  6015  off  6038  fnexALT  6055  fornex  6057  f1stres  6101  f2ndres  6102  xp1st  6107  xp2nd  6108  elxp6  6111  oprssdmm  6113  unielxp  6116  fmpox  6142  mpofvex  6145  opeliunxp2f  6179  dftpos4  6204  smoel  6241  tfrlem3-2d  6253  tfrlem8  6259  tfrlem9  6260  tfrlemibxssdm  6268  tfrlemi1  6273  tfrexlem  6275  tfr1onlemsucfn  6281  tfr1onlemsucaccv  6282  tfr1onlembxssdm  6284  tfr1onlembfn  6285  tfr1onlemaccex  6289  tfr1onlemres  6290  tfri1dALT  6292  tfrcllemsucfn  6294  tfrcllemsucaccv  6295  tfrcllembxssdm  6297  tfrcllembfn  6298  tfrcllemaccex  6302  tfrcllemres  6303  tfrcl  6305  rdgtfr  6315  rdgon  6327  frecabex  6339  frecabcl  6340  frecfcllem  6345  frecsuclem  6347  nnacl  6420  nnmcl  6421  nnmordi  6456  nnaordex  6467  nnm00  6469  erexb  6498  qliftfuns  6557  ixpsnval  6639  elixp2  6640  resixp  6671  mptelixpg  6672  elixpsn  6673  fundmen  6744  fopwdom  6774  xpf1o  6782  dif1en  6817  diffitest  6825  diffifi  6832  inffiexmid  6844  unfiexmid  6855  unfidisj  6859  fiintim  6866  xpfi  6867  ssfirab  6871  fnfi  6874  iunfidisj  6883  snexxph  6887  fidcenumlemr  6892  elfi2  6909  ctssdccl  7045  isnumi  7100  cc2lem  7169  cc3  7171  addnidpig  7239  indpi  7245  dfplpq2  7257  addclnq  7278  mulclnq  7279  nnnq0lem1  7349  addclnq0  7354  mulclnq0  7355  nqpnq0nq  7356  distrnq0  7362  prloc  7394  prarloclemlo  7397  prarloclem3  7400  prarloclem5  7403  genpml  7420  genpmu  7421  addnqprl  7432  addnqpru  7433  mulnqprl  7471  mulnqpru  7472  ltexprlemell  7501  ltexprlemelu  7502  ltexprlemdisj  7509  ltexprlemloc  7510  ltexprlemrl  7513  ltexprlemru  7515  ltexpri  7516  recexprlemm  7527  recexprlemdisj  7533  recexprlemloc  7534  recexprlem1ssl  7536  recexprlem1ssu  7537  recexpr  7541  addclsr  7656  mulclsr  7657  suplocsrlemb  7709  suplocsrlempr  7710  suplocsrlem  7711  suplocsr  7712  pitonn  7751  peano2nnnn  7756  axaddrcl  7768  axmulrcl  7770  peano5nnnn  7795  axpre-suploclemres  7804  negreb  8123  negf1o  8240  eqord1  8341  eqord2  8342  cju  8815  peano2nn  8828  nn1m1nn  8834  nnaddcl  8836  nnmulcl  8837  nnsub  8855  nndivtr  8858  un0addcl  9106  un0mulcl  9107  elnnnn0  9116  elz  9152  nnnegz  9153  znegclb  9183  zaddcllempos  9187  zaddcllemneg  9189  zaddcl  9190  nzadd  9202  zmulcl  9203  elz2  9218  zneo  9248  nneoor  9249  zeo  9252  peano5uzti  9255  zindd  9265  uzp1  9455  uzaddcl  9480  supinfneg  9489  infsupneg  9490  supminfex  9491  ublbneg  9504  eqreznegel  9505  negm  9506  qmulz  9514  qnegcl  9527  irradd  9537  irrmul  9538  fzrev2  9969  negqmod0  10212  frec2uzuzd  10283  frecuzrdgrrn  10289  frec2uzrdg  10290  frecuzrdgrcl  10291  frecuzrdgsuc  10295  frecuzrdgrclt  10296  frecuzrdgg  10297  frecuzrdgsuctlem  10304  iseqovex  10337  seq3val  10339  seqvalcd  10340  seq3-1  10341  seqf  10342  seq3p1  10343  seqovcd  10344  seqp1cd  10347  seq3clss  10348  monoord  10357  monoord2  10358  ser3mono  10359  seq3split  10360  seq3caopr3  10362  seq3caopr2  10363  iseqf1olemjpcl  10376  iseqf1olemqpcl  10377  iseqf1olemfvp  10378  seq3f1olemqsumkj  10379  seq3f1olemqsum  10381  seq3f1oleml  10384  seq3f1o  10385  seq3homo  10391  seq3z  10392  seq3distr  10394  ser3ge0  10398  expp1  10408  expcllem  10412  expcl2lemap  10413  m1expcl2  10423  facnn  10583  fac0  10584  fac1  10585  faccl  10591  facdiv  10594  facndiv  10595  bccmpl  10610  bcn2  10620  bccl  10623  focdmex  10643  fihasheqf1oi  10644  seq3coll  10695  shftlem  10698  shftf  10712  seq3shft  10720  cjval  10727  cjth  10728  remim  10742  uzin2  10869  caubnd2  10999  negfi  11109  xrmaxltsup  11137  clim  11160  clim2  11162  climshftlemg  11181  climcn1  11187  climcn2  11188  iserex  11218  climub  11223  climserle  11224  climcau  11226  serf0  11231  sumfct  11253  sumrbdclem  11256  fsum3cvg  11257  summodclem3  11259  summodclem2a  11260  zsumdc  11263  fsumgcl  11265  fsum3  11266  fsumf1o  11269  isumss  11270  isumss2  11272  fsum3cvg2  11273  fsum3ser  11276  fsumcl2lem  11277  fsumsplitf  11287  sumpr  11292  sumtp  11293  fsumm1  11295  fsum1p  11297  isummulc2  11305  fsum2dlemstep  11313  fisumcom2  11317  fsumshftm  11324  fisum0diag2  11326  fsummulc2  11327  fsumge1  11340  fsum00  11341  fsumabs  11344  telfsumo  11345  telfsumo2  11346  fsumparts  11349  fsumrelem  11350  fsumiun  11356  binomlem  11362  isumshft  11369  isum1p  11371  isumrpcl  11373  cvgratnnlemnexp  11403  cvgratnnlemmn  11404  cvgratnnlemseq  11405  cvgratnnlemabsle  11406  cvgratnnlemfm  11408  cvgratnnlemrate  11409  cvgratnn  11410  cvgratz  11411  mertenslem2  11415  mertensabs  11416  clim2prod  11418  prodfap0  11424  prodfrecap  11425  prodfdivap  11426  prodrbdclem  11450  fproddccvg  11451  prodmodclem3  11454  prodmodclem2a  11455  zproddc  11458  fprodseq  11462  prodfct  11466  fprodf1o  11467  prodssdc  11468  fprodssdc  11469  fprodmul  11470  fprodm1  11477  fprod1p  11478  fprodm1s  11480  fprodp1s  11481  fprodcl2lem  11484  fprodabs  11495  fprod2dlemstep  11501  fprodcnv  11504  fprodcom2fi  11505  fprodrec  11508  fproddivapf  11510  fprodsplitf  11511  fprodsplit1f  11513  fprodle  11519  zeo3  11740  mulsucdiv2z  11757  zob  11763  nn0o1gt2  11777  nno  11778  nn0o  11779  infssuzex  11817  infssuzcldc  11819  qnumdencl  12041  znnen  12099  ennnfonelemj0  12102  ennnfonelemg  12104  ennnfonelemom  12109  ctinfom  12129  ctiunctlemu1st  12135  ctiunctlemu2nd  12136  ctiunctlemudc  12138  ctiunctlemfo  12140  isstruct2im  12160  isstruct2r  12161  uniopn  12359  inopn  12361  fiinopn  12362  iscld  12463  iuncld  12475  tgrest  12529  iscn  12557  cnpval  12558  iscnp  12559  tgcn  12568  ssidcn  12570  lmbrf  12575  cnpnei  12579  cnima  12580  cnconst2  12593  cnrest2  12596  cnptopresti  12598  cnptoprest  12599  lmres  12608  lmtopcnp  12610  txbasval  12627  tx1cn  12629  tx2cn  12630  txcnp  12631  txcnmpt  12633  txdis1cn  12638  txlm  12639  cnmpt11  12643  cnmpt12  12647  cnmpt21  12651  cnmpt22  12654  ishmeo  12664  hmeoopn  12671  hmeocld  12672  qtopbasss  12881  fsumcncntop  12916  expcncf  12952  ivthinclemlopn  12974  ivthinclemlr  12975  ivthinclemuopn  12976  ivthinclemur  12977  ivthinclemdisj  12978  ivthinclemloc  12979  ivthinc  12981  ivthdec  12982  limccl  12988  ellimc3apf  12989  cnmptlimc  13003  limccoap  13007  2irrexpq  13253  2irrexpqap  13255  bdinex1g  13435  bj-intexr  13442  bj-prexg  13445  bj-uniex  13451  bj-uniexg  13452  bdunexb  13454  bj-indsuc  13462  exmidsbthrlem  13555  qdencn  13560  iswomni0  13584