Theorem eleqtrrdi 2299

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	|- ( ph -> A e. B )
eleqtrrdi.2	|- C = B

Assertion

Ref	Expression
eleqtrrdi	|- ( ph -> A e. C )

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrrdi.2	. . 3 |- C = B
3	2	eqcomi 2209	. 2 |- B = C
4	1, 3	eleqtrdi 2298	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  brelrng  4910  elabrex  5828  elabrexg  5829  fliftel1  5865  ovidig  6065  unielxp  6262  2oconcl  6527  ecopqsi  6679  eroprf  6717  exmidpweq  7008  sbthlem2  7062  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  caseinl  7195  caseinr  7196  ctssdccl  7215  isnumi  7291  addclnq  7490  mulclnq  7491  recexnq  7505  ltexnqq  7523  prarloclemarch  7533  prarloclemarch2  7534  nnnq  7537  nqnq0  7556  addclnq0  7566  mulclnq0  7567  nqpnq0nq  7568  prarloclemlt  7608  prarloclemlo  7609  prarloclemcalc  7617  nqprm  7657  cauappcvgprlem2  7775  caucvgprlem2  7795  addclsr  7868  mulclsr  7869  prsrcl  7899  mappsrprg  7919  suplocsrlemb  7921  pitonnlem2  7962  pitore  7965  recnnre  7966  axaddcl  7979  axmulcl  7981  axcaucvglemcl  8010  axcaucvglemval  8012  axcaucvglemcau  8013  axcaucvglemres  8014  uztrn2  9668  eluz2nn  9689  peano2uzs  9707  rebtwn2z  10399  seqf  10611  ser0  10680  bcm1k  10907  bcp1nk  10909  bcpasc  10913  hashennn  10927  hashcl  10928  climconst  11634  climshft2  11650  clim2ser  11681  clim2ser2  11682  iserex  11683  serf0  11696  zsumdc  11728  fsump1i  11777  iserabs  11819  isumshft  11834  isumsplit  11835  isum1p  11836  isumrpcl  11838  cvgratnnlemseq  11870  cvgratz  11876  cvgratgt0  11877  clim2prod  11883  clim2divap  11884  prodf1  11886  ntrivcvgap0  11893  zproddc  11923  fprodntrivap  11928  fprodabs  11960  fprodeq0  11961  ef0lem  12004  dvdsflip  12195  fzo0dvdseq  12201  bitsinv1  12306  gcdsupcl  12312  nninfctlemfo  12394  ialgr0  12399  prmind2  12475  crth  12579  prmdiv  12590  pockthlem  12712  pockthg  12713  prmunb  12718  ennnfonelemkh  12816  ennnfonelemrn  12823  ennnfonelemdm  12824  ctiunctlemf  12842  strslfv2d  12908  1strbas  12982  2strbasg  12985  2stropg  12986  2strbas1g  12988  rngbaseg  13001  rngplusgg  13002  rngmulrg  13003  srngbased  13012  srngplusgd  13013  srngmulrd  13014  srnginvld  13015  lmodbased  13030  lmodplusgd  13031  lmodscad  13032  lmodvscad  13033  ipsbased  13042  ipsaddgd  13043  ipsmulrd  13044  ipsscad  13045  ipsvscad  13046  ipsipd  13047  topgrpbasd  13062  topgrpplusgd  13063  topgrptsetd  13064  mulgnnp1  13499  znf1o  14446  lmconst  14721  lmss  14751  uptx  14779  cnmpt1res  14801  dvidlemap  15196  dvidrelem  15197  dvrecap  15218  plycolemc  15263  plycn  15267  pilem3  15288  logbleb  15466  logblt  15467  lgseisenlem1  15580  structvtxval  15669  djulclALT  15774  djurclALT  15775  pwle2  15972  trilpolemeq1  16016