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  fsn2g  5822  fressnfv  5841  fnex  5876  funfvima  5886  funfvima3  5888  f1mpt  5912  fliftfuns  5939  isoselem  5961  ovrspc2v  6044  ffnov  6125  fovcld  6126  ovmpos  6145  ov2gf  6146  ovg  6161  funimassov  6172  caovclg  6175  elovmpo  6221  off  6248  caofdig  6269  fnexALT  6273  focdmex  6277  f1stres  6322  f2ndres  6323  xp1st  6328  xp2nd  6329  elxp6  6332  oprssdmm  6334  unielxp  6337  fmpox  6365  mpofvex  6370  elmpom  6403  opeliunxp2f  6404  dftpos4  6429  smoel  6466  tfrlem3-2d  6478  tfrlem8  6484  tfrlem9  6485  tfrlemibxssdm  6493  tfrlemi1  6498  tfrexlem  6500  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  rdgtfr  6540  rdgon  6552  frecabex  6564  frecabcl  6565  frecfcllem  6570  frecsuclem  6572  nnacl  6648  nnmcl  6649  nnmordi  6684  nnaordex  6696  nnm00  6698  erexb  6727  qliftfuns  6788  ixpsnval  6870  elixp2  6871  resixp  6902  mptelixpg  6903  elixpsn  6904  fundmen  6981  fopwdom  7022  xpf1o  7030  dif1en  7068  diffitest  7076  diffifi  7083  inffiexmid  7098  unfiexmid  7110  unfidisj  7114  prfidceq  7120  fiintim  7123  xpfi  7124  ssfirab  7129  fnfi  7135  iunfidisj  7145  snexxph  7149  fidcenumlemr  7154  elfi2  7171  ctssdccl  7310  isnumi  7386  cc2lem  7485  cc3  7487  addnidpig  7556  indpi  7562  dfplpq2  7574  addclnq  7595  mulclnq  7596  nnnq0lem1  7666  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  distrnq0  7679  prloc  7711  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  genpml  7737  genpmu  7738  addnqprl  7749  addnqpru  7750  mulnqprl  7788  mulnqpru  7789  ltexprlemell  7818  ltexprlemelu  7819  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  ltexpri  7833  recexprlemm  7844  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexpr  7858  addclsr  7973  mulclsr  7974  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  suplocsr  8029  pitonn  8068  peano2nnnn  8073  axaddrcl  8085  axmulrcl  8087  peano5nnnn  8112  axpre-suploclemres  8121  negreb  8444  negf1o  8561  eqord1  8663  eqord2  8664  cju  9141  peano2nn  9155  nn1m1nn  9161  nnaddcl  9163  nnmulcl  9164  nnsub  9182  nndivtr  9185  un0addcl  9435  un0mulcl  9436  elnnnn0  9445  elz  9481  nnnegz  9482  znegclb  9512  zaddcllempos  9516  zaddcllemneg  9518  zaddcl  9519  nzadd  9532  zmulcl  9533  elz2  9551  zneo  9581  nneoor  9582  zeo  9585  peano5uzti  9588  zindd  9598  uzp1  9790  uzaddcl  9820  supinfneg  9829  infsupneg  9830  supminfex  9831  ublbneg  9847  eqreznegel  9848  negm  9849  qmulz  9857  qnegcl  9870  irradd  9880  irrmul  9881  fzrev2  10320  infssuzex  10494  infssuzcldc  10496  zsupssdc  10499  negqmod0  10594  frec2uzuzd  10665  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  xnn0nnen  10700  iseqovex  10721  seq3val  10723  seqvalcd  10724  seq3-1  10725  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3clss  10734  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1og  10784  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  ser3ge0  10799  expp1  10809  expcllem  10813  expcl2lemap  10814  m1expcl2  10824  facnn  10990  fac0  10991  fac1  10992  faccl  10998  facdiv  11001  facndiv  11002  bccmpl  11017  bcn2  11027  bccl  11030  fihasheqf1oi  11050  seq3coll  11107  ccatalpha  11194  reuccatpfxs1lem  11331  reuccatpfxs1  11332  shftlem  11394  shftf  11408  seq3shft  11416  cjval  11423  cjth  11424  remim  11438  uzin2  11565  caubnd2  11695  negfi  11806  xrmaxltsup  11836  clim  11859  clim2  11861  climshftlemg  11880  climcn1  11886  climcn2  11887  iserex  11917  climub  11922  climserle  11923  climcau  11925  serf0  11930  sumfct  11952  sumrbdclem  11956  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  zsumdc  11963  fsumgcl  11965  fsum3  11966  fsumf1o  11969  isumss  11970  isumss2  11972  fsum3cvg2  11973  fsum3ser  11976  fsumcl2lem  11977  fsumsplitf  11987  sumpr  11992  sumtp  11993  fsumm1  11995  fsum1p  11997  isummulc2  12005  fsum2dlemstep  12013  fisumcom2  12017  fsumshftm  12024  fisum0diag2  12026  fsummulc2  12027  fsumge1  12040  fsum00  12041  fsumabs  12044  telfsumo  12045  telfsumo2  12046  fsumparts  12049  fsumrelem  12050  fsumiun  12056  binomlem  12062  isumshft  12069  isum1p  12071  isumrpcl  12073  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratnn  12110  cvgratz  12111  mertenslem2  12115  mertensabs  12116  clim2prod  12118  prodfap0  12124  prodfrecap  12125  prodfdivap  12126  prodrbdclem  12150  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  prodfct  12166  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodmul  12170  fprodm1  12177  fprod1p  12178  fprodm1s  12180  fprodp1s  12181  fprodcl2lem  12184  fprodabs  12195  fprod2dlemstep  12201  fprodcnv  12204  fprodcom2fi  12205  fprodrec  12208  fproddivapf  12210  fprodsplitf  12211  fprodsplit1f  12213  fprodle  12219  zeo3  12447  mulsucdiv2z  12464  zob  12470  nn0o1gt2  12484  nno  12485  nn0o  12486  uzwodc  12626  qnumdencl  12777  pcqcl  12897  pcxnn0cl  12901  pcxcl  12902  pcgcd1  12919  dvdsprmpweqle  12928  pcmpt  12934  pcmpt2  12935  pcmptdvds  12936  infpnlem2  12951  1arith  12958  elgz  12962  mul4sq  12985  4sqlem13m  12994  4sqlem17  12998  4sqlem18  12999  4sqlem19  13000  znnen  13037  ennnfonelemj0  13040  ennnfonelemg  13042  ennnfonelemom  13047  ctinfom  13067  ctiunctlemu1st  13073  ctiunctlemu2nd  13074  ctiunctlemudc  13076  ctiunctlemfo  13078  ssnnctlemct  13085  infpn2  13095  isstruct2im  13110  isstruct2r  13111  imasaddfnlemg  13415  ercpbl  13432  xpsfrnel2  13447  mgmsscl  13462  mgm1  13471  sgrppropd  13514  mndpropd  13541  issubm  13573  0subm  13585  insubm  13586  mhmima  13592  mulgsubcl  13741  issubg  13778  subgex  13781  issubg2m  13794  issubg4m  13798  0subg  13804  isnsg  13807  isnsg2  13808  nsgbi  13809  isnsg3  13812  elnmz  13813  nmzbi  13814  nmzsubg  13815  nmznsg  13818  releqgg  13825  eqgex  13826  eqgval  13828  eqgid  13831  ghmrn  13862  ghmnsgima  13873  eqgabl  13935  ablnsg  13939  gsumfzmhm2  13949  isrng  13966  issrg  13997  srgfcl  14005  isring  14032  iscrng  14035  dvdsrd  14127  unitsubm  14152  isrim0  14194  issubrng  14232  subrngringnsg  14238  issubrng2  14243  opprsubrngg  14244  issubrg  14254  subrgsubm  14267  subrgugrp  14273  issubrg2  14274  issubrg3  14280  subrgpropd  14286  aprval  14315  aprsym  14317  islmod  14324  lmodlema  14325  islmodd  14326  lmodprop2d  14381  rmodislmodlem  14383  rmodislmod  14384  lsssetm  14389  islssmd  14392  lssclg  14397  lsslss  14414  lsspropdg  14464  islidlm  14512  rnglidlmcl  14513  isridlrng  14515  rnglidlmmgm  14529  isridl  14537  gsumfzfsumlemm  14620  psrbag  14702  psr1clfi  14721  uniopn  14744  inopn  14746  fiinopn  14747  iscld  14846  iuncld  14858  tgrest  14912  iscn  14940  cnpval  14941  iscnp  14942  tgcn  14951  ssidcn  14953  lmbrf  14958  cnpnei  14962  cnima  14963  cnconst2  14976  cnrest2  14979  cnptopresti  14981  cnptoprest  14982  lmres  14991  lmtopcnp  14993  txbasval  15010  tx1cn  15012  tx2cn  15013  txcnp  15014  txcnmpt  15016  txdis1cn  15021  txlm  15022  cnmpt11  15026  cnmpt12  15030  cnmpt21  15034  cnmpt22  15037  ishmeo  15047  hmeoopn  15054  hmeocld  15055  qtopbasss  15264  fsumcncntop  15310  expcn  15312  expcncf  15352  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemdisj  15383  ivthinclemloc  15384  ivthinc  15386  ivthdec  15387  limccl  15402  ellimc3apf  15403  cnmptlimc  15417  limccoap  15421  dvmptfsum  15468  plycolemc  15501  plycj  15504  2irrexpq  15719  2irrexpqap  15721  fsumdvdsmul  15734  perfect  15744  lgsval  15752  lgsval2lem  15758  lgsdir2lem4  15779  lgsdir2  15781  m1lgs  15833  2lgs  15852  mul2sq  15864  2sqlem6  15868  wlkcprim  16220  isclwwlk  16264  clwwlk1loop  16269  clwwlkccatlem  16270  clwwlkn1  16288  loopclwwlkn1b  16289  clwwlkn1loopb  16290  clwwlkn2  16291  clwwlkext2edg  16292  umgr2cwwk2dif  16294  s2elclwwlknon2  16306  clwwlknonex2lem2  16308  clwwlknonex2  16309  eupth2lem2dc  16329  eulerpathprum  16350  bdinex1g  16547  bj-intexr  16554  bj-prexg  16557  bj-uniex  16563  bj-uniexg  16564  bdunexb  16566  bj-indsuc  16574  exmidsbthrlem  16677  qdencn  16682  iswomni0  16707  gfsumval  16732  gfsumcl  16739