Theorem eleqtrrdi 2234

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  brelrng  4778  elabrex  5667  fliftel1  5703  ovidig  5896  unielxp  6080  2oconcl  6344  ecopqsi  6492  eroprf  6530  sbthlem2  6854  djulclr  6942  djurclr  6943  djulcl  6944  djurcl  6945  caseinl  6984  caseinr  6985  ctssdccl  7004  isnumi  7055  addclnq  7207  mulclnq  7208  recexnq  7222  ltexnqq  7240  prarloclemarch  7250  prarloclemarch2  7251  nnnq  7254  nqnq0  7273  addclnq0  7283  mulclnq0  7284  nqpnq0nq  7285  prarloclemlt  7325  prarloclemlo  7326  prarloclemcalc  7334  nqprm  7374  cauappcvgprlem2  7492  caucvgprlem2  7512  addclsr  7585  mulclsr  7586  prsrcl  7616  mappsrprg  7636  suplocsrlemb  7638  pitonnlem2  7679  pitore  7682  recnnre  7683  axaddcl  7696  axmulcl  7698  axcaucvglemcl  7727  axcaucvglemval  7729  axcaucvglemcau  7730  axcaucvglemres  7731  uztrn2  9367  eluz2nn  9388  peano2uzs  9406  rebtwn2z  10063  seqf  10265  ser0  10318  bcm1k  10538  bcp1nk  10540  bcpasc  10544  hashennn  10558  hashcl  10559  climconst  11091  climshft2  11107  clim2ser  11138  clim2ser2  11139  iserex  11140  serf0  11153  zsumdc  11185  fsump1i  11234  iserabs  11276  isumshft  11291  isumsplit  11292  isum1p  11293  isumrpcl  11295  cvgratnnlemseq  11327  cvgratz  11333  cvgratgt0  11334  clim2prod  11340  clim2divap  11341  prodf1  11343  ntrivcvgap0  11350  zproddc  11380  ef0lem  11403  dvdsflip  11585  fzo0dvdseq  11591  gcdsupcl  11683  ialgr0  11761  prmind2  11837  crth  11936  ennnfonelemkh  11961  ennnfonelemrn  11968  ennnfonelemdm  11969  ctiunctlemf  11987  strslfv2d  12040  1strbas  12097  2strbasg  12099  2stropg  12100  2strbas1g  12102  rngbaseg  12114  rngplusgg  12115  rngmulrg  12116  srngbased  12121  srngplusgd  12122  srngmulrd  12123  srnginvld  12124  lmodbased  12132  lmodplusgd  12133  lmodscad  12134  lmodvscad  12135  ipsbased  12140  ipsaddgd  12141  ipsmulrd  12142  ipsscad  12143  ipsvscad  12144  ipsipd  12145  topgrpbasd  12150  topgrpplusgd  12151  topgrptsetd  12152  lmconst  12424  lmss  12454  uptx  12482  cnmpt1res  12504  dvidlemap  12868  dvrecap  12885  pilem3  12912  logbleb  13086  logblt  13087  djulclALT  13179  djurclALT  13180  pwle2  13366  trilpolemeq1  13408