Theorem eleqtrrdi 2269

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2146

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  brelrng  4851  elabrex  5749  fliftel1  5785  ovidig  5982  unielxp  6165  2oconcl  6430  ecopqsi  6580  eroprf  6618  exmidpweq  6899  sbthlem2  6947  djulclr  7038  djurclr  7039  djulcl  7040  djurcl  7041  caseinl  7080  caseinr  7081  ctssdccl  7100  isnumi  7171  addclnq  7349  mulclnq  7350  recexnq  7364  ltexnqq  7382  prarloclemarch  7392  prarloclemarch2  7393  nnnq  7396  nqnq0  7415  addclnq0  7425  mulclnq0  7426  nqpnq0nq  7427  prarloclemlt  7467  prarloclemlo  7468  prarloclemcalc  7476  nqprm  7516  cauappcvgprlem2  7634  caucvgprlem2  7654  addclsr  7727  mulclsr  7728  prsrcl  7758  mappsrprg  7778  suplocsrlemb  7780  pitonnlem2  7821  pitore  7824  recnnre  7825  axaddcl  7838  axmulcl  7840  axcaucvglemcl  7869  axcaucvglemval  7871  axcaucvglemcau  7872  axcaucvglemres  7873  uztrn2  9518  eluz2nn  9539  peano2uzs  9557  rebtwn2z  10225  seqf  10431  ser0  10484  bcm1k  10708  bcp1nk  10710  bcpasc  10714  hashennn  10728  hashcl  10729  climconst  11266  climshft2  11282  clim2ser  11313  clim2ser2  11314  iserex  11315  serf0  11328  zsumdc  11360  fsump1i  11409  iserabs  11451  isumshft  11466  isumsplit  11467  isum1p  11468  isumrpcl  11470  cvgratnnlemseq  11502  cvgratz  11508  cvgratgt0  11509  clim2prod  11515  clim2divap  11516  prodf1  11518  ntrivcvgap0  11525  zproddc  11555  fprodntrivap  11560  fprodabs  11592  fprodeq0  11593  ef0lem  11636  dvdsflip  11824  fzo0dvdseq  11830  gcdsupcl  11926  ialgr0  12011  prmind2  12087  crth  12191  prmdiv  12202  pockthlem  12321  pockthg  12322  prmunb  12327  ennnfonelemkh  12380  ennnfonelemrn  12387  ennnfonelemdm  12388  ctiunctlemf  12406  strslfv2d  12471  1strbas  12539  2strbasg  12541  2stropg  12542  2strbas1g  12544  rngbaseg  12556  rngplusgg  12557  rngmulrg  12558  srngbased  12563  srngplusgd  12564  srngmulrd  12565  srnginvld  12566  lmodbased  12577  lmodplusgd  12578  lmodscad  12579  lmodvscad  12580  ipsbased  12585  ipsaddgd  12586  ipsmulrd  12587  ipsscad  12588  ipsvscad  12589  ipsipd  12590  topgrpbasd  12602  topgrpplusgd  12603  topgrptsetd  12604  mulgnnp1  12861  lmconst  13296  lmss  13326  uptx  13354  cnmpt1res  13376  dvidlemap  13740  dvrecap  13757  pilem3  13784  logbleb  13959  logblt  13960  djulclALT  14122  djurclALT  14123  pwle2  14317  trilpolemeq1  14358