Theorem eleq1d 2300

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

Hypothesis

Ref	Expression
eleq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eleq1d	|- ( ph -> ( A e. C <-> B e. C ) )

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- ( ph -> A = B )
2		eleq1 2294	. 2 |- ( A = B -> ( A e. C <-> B e. C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   e. wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eqeltrd  2308  eqneltrd  2327  eqneltrrd  2328  rspcimdv  2911  rspcimedv  2912  reuind  3011  sbcel2g  3148  sbccsb2g  3157  breq1  4091  breq2  4092  inex1g  4225  intexr  4240  pwexg  4270  prexg  4301  opelopabsb  4354  pofun  4409  seex  4432  uniex  4534  uniexg  4536  unexb  4539  abnexg  4543  reusv3  4557  rabxfrd  4566  onun2  4588  onsucelsucexmid  4628  ordsucunielexmid  4629  dcextest  4679  tfisi  4685  peano2  4693  seinxp  4797  opabid2  4861  opeliunxp2  4870  elrn2g  4920  opeldm  4934  opeldmg  4936  elreldm  4958  elrn2  4974  opelresg  5020  elsnres  5050  iss  5059  elimasng  5104  issref  5119  rnxpid  5171  unielrel  5264  dffun5r  5338  funopg  5360  brprcneu  5632  tz6.12f  5668  fvelrnb  5693  ssimaex  5707  dmfco  5714  fvmpt3  5725  mptfvex  5732  fvmptf  5739  respreima  5775  fvelrn  5778  ffnfvf  5806  ffvresb  5810  fmptco  5813  fmptcof  5814  fsn  5819  fressnfv  5840  fnex  5875  funfvima  5885  funfvima3  5887  f1mpt  5911  fliftfuns  5938  isoselem  5960  ovrspc2v  6043  ffnov  6124  fovcld  6125  ovmpos  6144  ov2gf  6145  ovg  6160  funimassov  6171  caovclg  6174  elovmpo  6220  off  6247  caofdig  6268  fnexALT  6272  focdmex  6276  f1stres  6321  f2ndres  6322  xp1st  6327  xp2nd  6328  elxp6  6331  oprssdmm  6333  unielxp  6336  fmpox  6364  mpofvex  6369  elmpom  6402  opeliunxp2f  6403  dftpos4  6428  smoel  6465  tfrlem3-2d  6477  tfrlem8  6483  tfrlem9  6484  tfrlemibxssdm  6492  tfrlemi1  6497  tfrexlem  6499  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfr1onlemres  6514  tfri1dALT  6516  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  rdgtfr  6539  rdgon  6551  frecabex  6563  frecabcl  6564  frecfcllem  6569  frecsuclem  6571  nnacl  6647  nnmcl  6648  nnmordi  6683  nnaordex  6695  nnm00  6697  erexb  6726  qliftfuns  6787  ixpsnval  6869  elixp2  6870  resixp  6901  mptelixpg  6902  elixpsn  6903  fundmen  6980  fopwdom  7021  xpf1o  7029  dif1en  7067  diffitest  7075  diffifi  7082  inffiexmid  7097  unfiexmid  7109  unfidisj  7113  prfidceq  7119  fiintim  7122  xpfi  7123  ssfirab  7128  fnfi  7134  iunfidisj  7144  snexxph  7148  fidcenumlemr  7153  elfi2  7170  ctssdccl  7309  isnumi  7385  cc2lem  7484  cc3  7486  addnidpig  7555  indpi  7561  dfplpq2  7573  addclnq  7594  mulclnq  7595  nnnq0lem1  7665  addclnq0  7670  mulclnq0  7671  nqpnq0nq  7672  distrnq0  7678  prloc  7710  prarloclemlo  7713  prarloclem3  7716  prarloclem5  7719  genpml  7736  genpmu  7737  addnqprl  7748  addnqpru  7749  mulnqprl  7787  mulnqpru  7788  ltexprlemell  7817  ltexprlemelu  7818  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  ltexpri  7832  recexprlemm  7843  recexprlemdisj  7849  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  recexpr  7857  addclsr  7972  mulclsr  7973  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  suplocsr  8028  pitonn  8067  peano2nnnn  8072  axaddrcl  8084  axmulrcl  8086  peano5nnnn  8111  axpre-suploclemres  8120  negreb  8443  negf1o  8560  eqord1  8662  eqord2  8663  cju  9140  peano2nn  9154  nn1m1nn  9160  nnaddcl  9162  nnmulcl  9163  nnsub  9181  nndivtr  9184  un0addcl  9434  un0mulcl  9435  elnnnn0  9444  elz  9480  nnnegz  9481  znegclb  9511  zaddcllempos  9515  zaddcllemneg  9517  zaddcl  9518  nzadd  9531  zmulcl  9532  elz2  9550  zneo  9580  nneoor  9581  zeo  9584  peano5uzti  9587  zindd  9597  uzp1  9789  uzaddcl  9819  supinfneg  9828  infsupneg  9829  supminfex  9830  ublbneg  9846  eqreznegel  9847  negm  9848  qmulz  9856  qnegcl  9869  irradd  9879  irrmul  9880  fzrev2  10319  infssuzex  10492  infssuzcldc  10494  zsupssdc  10497  negqmod0  10592  frec2uzuzd  10663  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgsuctlem  10684  xnn0nnen  10698  iseqovex  10719  seq3val  10721  seqvalcd  10722  seq3-1  10723  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3clss  10732  monoord  10746  monoord2  10747  ser3mono  10748  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  seqf1og  10782  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  ser3ge0  10797  expp1  10807  expcllem  10811  expcl2lemap  10812  m1expcl2  10822  facnn  10988  fac0  10989  fac1  10990  faccl  10996  facdiv  10999  facndiv  11000  bccmpl  11015  bcn2  11025  bccl  11028  fihasheqf1oi  11048  seq3coll  11105  ccatalpha  11189  reuccatpfxs1lem  11326  reuccatpfxs1  11327  shftlem  11376  shftf  11390  seq3shft  11398  cjval  11405  cjth  11406  remim  11420  uzin2  11547  caubnd2  11677  negfi  11788  xrmaxltsup  11818  clim  11841  clim2  11843  climshftlemg  11862  climcn1  11868  climcn2  11869  iserex  11899  climub  11904  climserle  11905  climcau  11907  serf0  11912  sumfct  11934  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsumgcl  11946  fsum3  11947  fsumf1o  11950  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumsplitf  11968  sumpr  11973  sumtp  11974  fsumm1  11976  fsum1p  11978  isummulc2  11986  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fisum0diag2  12007  fsummulc2  12008  fsumge1  12021  fsum00  12022  fsumabs  12025  telfsumo  12026  telfsumo2  12027  fsumparts  12030  fsumrelem  12031  fsumiun  12037  binomlem  12043  isumshft  12050  isum1p  12052  isumrpcl  12054  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  cvgratz  12092  mertenslem2  12096  mertensabs  12097  clim2prod  12099  prodfap0  12105  prodfrecap  12106  prodfdivap  12107  prodrbdclem  12131  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  prodfct  12147  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodmul  12151  fprodm1  12158  fprod1p  12159  fprodm1s  12161  fprodp1s  12162  fprodcl2lem  12165  fprodabs  12176  fprod2dlemstep  12182  fprodcnv  12185  fprodcom2fi  12186  fprodrec  12189  fproddivapf  12191  fprodsplitf  12192  fprodsplit1f  12194  fprodle  12200  zeo3  12428  mulsucdiv2z  12445  zob  12451  nn0o1gt2  12465  nno  12466  nn0o  12467  uzwodc  12607  qnumdencl  12758  pcqcl  12878  pcxnn0cl  12882  pcxcl  12883  pcgcd1  12900  dvdsprmpweqle  12909  pcmpt  12915  pcmpt2  12916  pcmptdvds  12917  infpnlem2  12932  1arith  12939  elgz  12943  mul4sq  12966  4sqlem13m  12975  4sqlem17  12979  4sqlem18  12980  4sqlem19  12981  znnen  13018  ennnfonelemj0  13021  ennnfonelemg  13023  ennnfonelemom  13028  ctinfom  13048  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  ctiunctlemudc  13057  ctiunctlemfo  13059  ssnnctlemct  13066  infpn2  13076  isstruct2im  13091  isstruct2r  13092  imasaddfnlemg  13396  ercpbl  13413  xpsfrnel2  13428  mgmsscl  13443  mgm1  13452  sgrppropd  13495  mndpropd  13522  issubm  13554  0subm  13566  insubm  13567  mhmima  13573  mulgsubcl  13722  issubg  13759  subgex  13762  issubg2m  13775  issubg4m  13779  0subg  13785  isnsg  13788  isnsg2  13789  nsgbi  13790  isnsg3  13793  elnmz  13794  nmzbi  13795  nmzsubg  13796  nmznsg  13799  releqgg  13806  eqgex  13807  eqgval  13809  eqgid  13812  ghmrn  13843  ghmnsgima  13854  eqgabl  13916  ablnsg  13920  gsumfzmhm2  13930  isrng  13946  issrg  13977  srgfcl  13985  isring  14012  iscrng  14015  dvdsrd  14107  unitsubm  14132  isrim0  14174  issubrng  14212  subrngringnsg  14218  issubrng2  14223  opprsubrngg  14224  issubrg  14234  subrgsubm  14247  subrgugrp  14253  issubrg2  14254  issubrg3  14260  subrgpropd  14266  aprval  14295  aprsym  14297  islmod  14304  lmodlema  14305  islmodd  14306  lmodprop2d  14361  rmodislmodlem  14363  rmodislmod  14364  lsssetm  14369  islssmd  14372  lssclg  14377  lsslss  14394  lsspropdg  14444  islidlm  14492  rnglidlmcl  14493  isridlrng  14495  rnglidlmmgm  14509  isridl  14517  gsumfzfsumlemm  14600  psrbag  14682  psr1clfi  14701  uniopn  14724  inopn  14726  fiinopn  14727  iscld  14826  iuncld  14838  tgrest  14892  iscn  14920  cnpval  14921  iscnp  14922  tgcn  14931  ssidcn  14933  lmbrf  14938  cnpnei  14942  cnima  14943  cnconst2  14956  cnrest2  14959  cnptopresti  14961  cnptoprest  14962  lmres  14971  lmtopcnp  14973  txbasval  14990  tx1cn  14992  tx2cn  14993  txcnp  14994  txcnmpt  14996  txdis1cn  15001  txlm  15002  cnmpt11  15006  cnmpt12  15010  cnmpt21  15014  cnmpt22  15017  ishmeo  15027  hmeoopn  15034  hmeocld  15035  qtopbasss  15244  fsumcncntop  15290  expcn  15292  expcncf  15332  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  ivthinc  15366  ivthdec  15367  limccl  15382  ellimc3apf  15383  cnmptlimc  15397  limccoap  15401  dvmptfsum  15448  plycolemc  15481  plycj  15484  2irrexpq  15699  2irrexpqap  15701  fsumdvdsmul  15714  perfect  15724  lgsval  15732  lgsval2lem  15738  lgsdir2lem4  15759  lgsdir2  15761  m1lgs  15813  2lgs  15832  mul2sq  15844  2sqlem6  15848  wlkcprim  16200  isclwwlk  16244  clwwlk1loop  16249  clwwlkccatlem  16250  clwwlkn1  16268  loopclwwlkn1b  16269  clwwlkn1loopb  16270  clwwlkn2  16271  clwwlkext2edg  16272  umgr2cwwk2dif  16274  s2elclwwlknon2  16286  clwwlknonex2lem2  16288  clwwlknonex2  16289  eupth2lem2dc  16309  bdinex1g  16496  bj-intexr  16503  bj-prexg  16506  bj-uniex  16512  bj-uniexg  16513  bdunexb  16515  bj-indsuc  16523  exmidsbthrlem  16626  qdencn  16631  iswomni0  16655  gfsumval  16680