Theorem eleq1d 2303

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 2297	. 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 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  eleq12d  2305  eqeltrd  2311  eqneltrd  2330  eqneltrrd  2331  rspcimdv  2924  rspcimedv  2925  reuind  3025  sbcel2g  3162  sbccsb2g  3171  breq1  4117  breq2  4118  inex1g  4251  intexr  4267  pwexg  4298  prexg  4330  opelopabsb  4383  pofun  4438  seex  4461  uniex  4563  uniexg  4565  unexb  4568  abnexg  4572  reusv3  4586  rabxfrd  4595  onun2  4617  onsucelsucexmid  4657  ordsucunielexmid  4658  dcextest  4708  tfisi  4714  peano2  4722  seinxp  4826  opabid2  4891  opeliunxp2  4900  elrn2g  4950  opeldm  4964  opeldmg  4966  elreldm  4988  elrn2  5004  opelresg  5050  elsnres  5080  iss  5089  xpexcnvm  5122  elimasng  5135  issref  5150  rnxpid  5202  unielrel  5295  dffun5r  5369  funopg  5391  brprcneu  5668  tz6.12f  5704  fvelrnb  5729  ssimaex  5743  dmfco  5750  fvmpt3  5761  mptfvex  5768  fvmptf  5775  respreima  5810  fvelrn  5813  ffnfvf  5841  ffvresb  5845  fmptco  5848  fmptcof  5849  fsn  5854  fsn2g  5857  fressnfv  5876  fnex  5911  funfvima  5923  funfvima3  5925  f1mpt  5950  fliftfuns  5977  isoselem  5999  ovrspc2v  6084  ffnov  6165  fovcld  6166  ovmpos  6185  ov2gf  6186  ovg  6201  funimassov  6212  caovclg  6215  elovmpo  6261  off  6288  caofdig  6309  fnexALT  6313  focdmex  6317  f1stres  6366  f2ndres  6367  xp1st  6372  xp2nd  6373  elxp6  6376  oprssdmm  6378  unielxp  6381  fmpox  6409  mpofvex  6414  elmpom  6447  suppofss1dcl  6477  suppofss2dcl  6478  opeliunxp2f  6482  dftpos4  6507  smoel  6544  tfrlem3-2d  6556  tfrlem8  6562  tfrlem9  6563  tfrlemibxssdm  6571  tfrlemi1  6576  tfrexlem  6578  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfr1onlemres  6593  tfri1dALT  6595  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  rdgtfr  6618  rdgon  6630  frecabex  6642  frecabcl  6643  frecfcllem  6648  frecsuclem  6650  nnacl  6726  nnmcl  6727  nnmordi  6762  nnaordex  6774  nnm00  6776  erexb  6805  qliftfuns  6866  ixpsnval  6949  elixp2  6950  resixp  6981  mptelixpg  6982  elixpsn  6983  fundmen  7060  fopwdom  7102  xpf1o  7110  dif1en  7149  diffitest  7157  diffifi  7164  inffiexmid  7179  unfiexmid  7191  unfidisj  7195  prfidceq  7201  fiintim  7204  xpfi  7205  ssfirab  7210  fnfi  7216  iunfidisj  7226  mapfi  7227  snexxph  7233  fidcenumlemr  7238  isfsupp  7255  ffsuppbi  7266  elfi2  7272  ctssdccl  7415  isnumi  7491  cc2lem  7596  cc3  7598  addnidpig  7667  indpi  7673  dfplpq2  7685  addclnq  7706  mulclnq  7707  nnnq0lem1  7777  addclnq0  7782  mulclnq0  7783  nqpnq0nq  7784  distrnq0  7790  prloc  7822  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  genpml  7848  genpmu  7849  addnqprl  7860  addnqpru  7861  mulnqprl  7899  mulnqpru  7900  ltexprlemell  7929  ltexprlemelu  7930  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  ltexpri  7944  recexprlemm  7955  recexprlemdisj  7961  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  recexpr  7969  addclsr  8084  mulclsr  8085  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  suplocsr  8140  pitonn  8179  peano2nnnn  8184  axaddrcl  8196  axmulrcl  8198  peano5nnnn  8223  axpre-suploclemres  8232  negreb  8554  negf1o  8672  eqord1  8774  eqord2  8775  cju  9252  peano2nn  9266  nn1m1nn  9272  nnaddcl  9274  nnmulcl  9275  nnsub  9293  nndivtr  9296  un0addcl  9546  un0mulcl  9547  elnnnn0  9556  fcdmnn0fsuppg  9568  elz  9596  nnnegz  9597  znegclb  9627  zaddcllempos  9631  zaddcllemneg  9633  zaddcl  9634  nzadd  9647  zmulcl  9648  elz2  9666  zneo  9697  nneoor  9698  zeo  9701  peano5uzti  9704  zindd  9714  uzp1  9906  uzaddcl  9936  supinfneg  9945  infsupneg  9946  supminfex  9947  ublbneg  9963  eqreznegel  9964  negm  9965  qmulz  9973  qnegcl  9986  irradd  9996  irrmul  9997  fzsplit3  10407  fzspl  10425  fzrev2  10441  infssuzex  10615  infssuzcldc  10617  zsupssdc  10622  negqmod0  10717  frec2uzuzd  10788  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgsuctlem  10809  xnn0nnen  10823  iseqovex  10844  seq3val  10846  seqvalcd  10847  seq3-1  10848  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3clss  10857  monoord  10871  monoord2  10872  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  seqf1og  10907  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  ser3ge0  10922  expp1  10932  expcllem  10936  expcl2lemap  10937  m1expcl2  10947  facnn  11114  fac0  11115  fac1  11116  faccl  11122  facdiv  11125  facndiv  11126  bccmpl  11141  bcn2  11151  bccl  11154  fihasheqf1oi  11175  seq3coll  11239  ccatalpha  11326  reuccatpfxs1lem  11463  reuccatpfxs1  11464  shftlem  11526  shftf  11540  seq3shft  11548  cjval  11555  cjth  11556  remim  11570  uzin2  11697  caubnd2  11827  negfi  11938  xrmaxltsup  11968  clim  11991  clim2  11993  climshftlemg  12012  climcn1  12018  climcn2  12019  iserex  12049  climub  12054  climserle  12055  climcau  12057  serf0  12062  sumfct  12084  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumgcl  12097  fsum3  12098  fsumf1o  12101  isumss  12102  isumss2  12104  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumsplitf  12119  sumpr  12124  sumtp  12125  fsumm1  12127  fsum1p  12129  isummulc2  12137  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fisum0diag2  12158  fsummulc2  12159  fsumge1  12172  fsum00  12173  fsumabs  12176  telfsumo  12177  telfsumo2  12178  fsumparts  12181  fsumrelem  12182  fsumiun  12188  binomlem  12194  isumshft  12201  isum1p  12203  isumrpcl  12205  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  cvgratz  12243  mertenslem2  12247  mertensabs  12248  clim2prod  12250  prodfap0  12256  prodfrecap  12257  prodfdivap  12258  prodrbdclem  12282  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  prodfct  12298  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  fprodm1  12309  fprod1p  12310  fprodm1s  12312  fprodp1s  12313  fprodcl2lem  12316  fprodabs  12327  fprod2dlemstep  12333  fprodcnv  12336  fprodcom2fi  12337  fprodrec  12340  fproddivapf  12342  fprodsplitf  12343  fprodsplit1f  12345  fprodle  12351  zeo3  12579  mulsucdiv2z  12596  zob  12602  nn0o1gt2  12616  nno  12617  nn0o  12618  uzwodc  12758  qnumdencl  12909  pcqcl  13029  pcxnn0cl  13033  pcxcl  13034  pcgcd1  13051  dvdsprmpweqle  13060  pcmpt  13066  pcmpt2  13067  pcmptdvds  13068  infpnlem2  13083  1arith  13090  elgz  13094  mul4sq  13117  4sqlem13m  13126  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  ballotfilemsdom  13199  ballotfilemrv  13207  ballotfilemrv1  13208  ballotfilemrv2  13209  ballotfilem1ri  13222  znnen  13233  ennnfonelemj0  13236  ennnfonelemg  13238  ennnfonelemom  13243  ctinfom  13263  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunctlemfo  13274  ssnnctlemct  13281  infpn2  13291  isstruct2im  13306  isstruct2r  13307  imasaddfnlemg  13578  ercpbl  13595  xpsfrnel2  13610  mgmsscl  13624  mgm1  13633  sgrppropd  13676  mndpropd  13701  issubm  13727  0subm  13739  insubm  13740  mhmima  13746  mulgsubcl  13889  issubg  13926  subgex  13929  issubg2m  13942  issubg4m  13946  0subg  13952  isnsg  13955  isnsg2  13956  nsgbi  13957  isnsg3  13960  elnmz  13961  nmzbi  13962  nmzsubg  13963  nmznsg  13966  releqgg  13973  eqgex  13974  eqgval  13976  eqgid  13979  ghmrn  14010  ghmnsgima  14021  eqgabl  14083  ablnsg  14087  gsumfzmhm2  14097  gfsumval  14102  gfsumcl  14110  isrng  14173  issrg  14208  srgfcl  14216  isring  14243  iscrng  14246  dvdsrd  14339  unitsubm  14364  isrim0  14406  issubrng  14445  subrngringnsg  14451  issubrng2  14456  opprsubrngg  14457  issubrg  14467  subrgsubm  14480  subrgugrp  14486  issubrg2  14487  issubrg3  14493  subrgpropd  14499  aprval  14529  aprunit  14530  aprsym  14534  opprdrng  14558  islmod  14565  lmodlema  14566  islmodd  14567  lmodprop2d  14622  rmodislmodlem  14624  rmodislmod  14625  lsssetm  14630  islssmd  14633  lssclg  14638  lsslss  14655  lsspropdg  14705  islidlm  14753  rnglidlmcl  14754  isridlrng  14756  rnglidlmmgm  14770  isridl  14778  gsumfzfsumlemm  14861  psrbag  14943  psr1clfi  14969  uniopn  14992  inopn  14994  fiinopn  14995  iscld  15094  iuncld  15106  tgrest  15160  iscn  15188  cnpval  15189  iscnp  15190  tgcn  15199  ssidcn  15201  lmbrf  15206  cnpnei  15210  cnima  15211  cnconst2  15224  cnrest2  15227  cnptopresti  15229  cnptoprest  15230  lmres  15239  lmtopcnp  15241  txbasval  15258  tx1cn  15260  tx2cn  15261  txcnp  15262  txcnmpt  15264  txdis1cn  15269  txlm  15270  cnmpt11  15274  cnmpt12  15278  cnmpt21  15282  cnmpt22  15285  ishmeo  15295  hmeoopn  15302  hmeocld  15303  qtopbasss  15512  fsumcncntop  15558  expcn  15560  expcncf  15600  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  ivthinc  15634  ivthdec  15635  limccl  15650  ellimc3apf  15651  cnmptlimc  15665  limccoap  15669  dvmptfsum  15716  plycolemc  15749  plycj  15752  2irrexpq  15967  2irrexpqap  15969  pellexlem1  15971  fsumdvdsmul  15985  perfect  15995  lgsval  16003  lgsval2lem  16009  lgsdir2lem4  16030  lgsdir2  16032  m1lgs  16084  2lgs  16103  mul2sq  16115  2sqlem6  16119  wlkcprim  16471  isclwwlk  16515  clwwlk1loop  16520  clwwlkccatlem  16521  clwwlkn1  16539  loopclwwlkn1b  16540  clwwlkn1loopb  16541  clwwlkn2  16542  clwwlkext2edg  16543  umgr2cwwk2dif  16545  s2elclwwlknon2  16557  clwwlknonex2lem2  16559  clwwlknonex2  16560  eupth2lem2dc  16580  eulerpathprum  16601  bdinex1g  16797  bj-intexr  16804  bj-prexg  16807  bj-uniex  16813  bj-uniexg  16814  bdunexb  16816  bj-indsuc  16824  exmidsbthrlem  16928  qdencn  16933  repiecef  16938  iswomni0  16962