Theorem eleqtrrdi 2290

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 2200	. 2 |- B = C
4	1, 3	eleqtrdi 2289	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  brelrng  4898  elabrex  5807  elabrexg  5808  fliftel1  5844  ovidig  6044  unielxp  6241  2oconcl  6506  ecopqsi  6658  eroprf  6696  exmidpweq  6979  sbthlem2  7033  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  caseinl  7166  caseinr  7167  ctssdccl  7186  isnumi  7260  addclnq  7459  mulclnq  7460  recexnq  7474  ltexnqq  7492  prarloclemarch  7502  prarloclemarch2  7503  nnnq  7506  nqnq0  7525  addclnq0  7535  mulclnq0  7536  nqpnq0nq  7537  prarloclemlt  7577  prarloclemlo  7578  prarloclemcalc  7586  nqprm  7626  cauappcvgprlem2  7744  caucvgprlem2  7764  addclsr  7837  mulclsr  7838  prsrcl  7868  mappsrprg  7888  suplocsrlemb  7890  pitonnlem2  7931  pitore  7934  recnnre  7935  axaddcl  7948  axmulcl  7950  axcaucvglemcl  7979  axcaucvglemval  7981  axcaucvglemcau  7982  axcaucvglemres  7983  uztrn2  9636  eluz2nn  9657  peano2uzs  9675  rebtwn2z  10361  seqf  10573  ser0  10642  bcm1k  10869  bcp1nk  10871  bcpasc  10875  hashennn  10889  hashcl  10890  climconst  11472  climshft2  11488  clim2ser  11519  clim2ser2  11520  iserex  11521  serf0  11534  zsumdc  11566  fsump1i  11615  iserabs  11657  isumshft  11672  isumsplit  11673  isum1p  11674  isumrpcl  11676  cvgratnnlemseq  11708  cvgratz  11714  cvgratgt0  11715  clim2prod  11721  clim2divap  11722  prodf1  11724  ntrivcvgap0  11731  zproddc  11761  fprodntrivap  11766  fprodabs  11798  fprodeq0  11799  ef0lem  11842  dvdsflip  12033  fzo0dvdseq  12039  bitsinv1  12144  gcdsupcl  12150  nninfctlemfo  12232  ialgr0  12237  prmind2  12313  crth  12417  prmdiv  12428  pockthlem  12550  pockthg  12551  prmunb  12556  ennnfonelemkh  12654  ennnfonelemrn  12661  ennnfonelemdm  12662  ctiunctlemf  12680  strslfv2d  12746  1strbas  12820  2strbasg  12822  2stropg  12823  2strbas1g  12825  rngbaseg  12838  rngplusgg  12839  rngmulrg  12840  srngbased  12849  srngplusgd  12850  srngmulrd  12851  srnginvld  12852  lmodbased  12867  lmodplusgd  12868  lmodscad  12869  lmodvscad  12870  ipsbased  12879  ipsaddgd  12880  ipsmulrd  12881  ipsscad  12882  ipsvscad  12883  ipsipd  12884  topgrpbasd  12899  topgrpplusgd  12900  topgrptsetd  12901  mulgnnp1  13336  znf1o  14283  lmconst  14536  lmss  14566  uptx  14594  cnmpt1res  14616  dvidlemap  15011  dvidrelem  15012  dvrecap  15033  plycolemc  15078  plycn  15082  pilem3  15103  logbleb  15281  logblt  15282  lgseisenlem1  15395  djulclALT  15531  djurclALT  15532  pwle2  15729  trilpolemeq1  15771