Theorem eleqtrrdi 2287

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  brelrng  4893  elabrex  5800  elabrexg  5801  fliftel1  5837  ovidig  6036  unielxp  6227  2oconcl  6492  ecopqsi  6644  eroprf  6682  exmidpweq  6965  sbthlem2  7017  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  caseinl  7150  caseinr  7151  ctssdccl  7170  isnumi  7242  addclnq  7435  mulclnq  7436  recexnq  7450  ltexnqq  7468  prarloclemarch  7478  prarloclemarch2  7479  nnnq  7482  nqnq0  7501  addclnq0  7511  mulclnq0  7512  nqpnq0nq  7513  prarloclemlt  7553  prarloclemlo  7554  prarloclemcalc  7562  nqprm  7602  cauappcvgprlem2  7720  caucvgprlem2  7740  addclsr  7813  mulclsr  7814  prsrcl  7844  mappsrprg  7864  suplocsrlemb  7866  pitonnlem2  7907  pitore  7910  recnnre  7911  axaddcl  7924  axmulcl  7926  axcaucvglemcl  7955  axcaucvglemval  7957  axcaucvglemcau  7958  axcaucvglemres  7959  uztrn2  9610  eluz2nn  9631  peano2uzs  9649  rebtwn2z  10323  seqf  10535  ser0  10604  bcm1k  10831  bcp1nk  10833  bcpasc  10837  hashennn  10851  hashcl  10852  climconst  11433  climshft2  11449  clim2ser  11480  clim2ser2  11481  iserex  11482  serf0  11495  zsumdc  11527  fsump1i  11576  iserabs  11618  isumshft  11633  isumsplit  11634  isum1p  11635  isumrpcl  11637  cvgratnnlemseq  11669  cvgratz  11675  cvgratgt0  11676  clim2prod  11682  clim2divap  11683  prodf1  11685  ntrivcvgap0  11692  zproddc  11722  fprodntrivap  11727  fprodabs  11759  fprodeq0  11760  ef0lem  11803  dvdsflip  11993  fzo0dvdseq  11999  gcdsupcl  12095  nninfctlemfo  12177  ialgr0  12182  prmind2  12258  crth  12362  prmdiv  12373  pockthlem  12494  pockthg  12495  prmunb  12500  ennnfonelemkh  12569  ennnfonelemrn  12576  ennnfonelemdm  12577  ctiunctlemf  12595  strslfv2d  12661  1strbas  12735  2strbasg  12737  2stropg  12738  2strbas1g  12740  rngbaseg  12753  rngplusgg  12754  rngmulrg  12755  srngbased  12764  srngplusgd  12765  srngmulrd  12766  srnginvld  12767  lmodbased  12782  lmodplusgd  12783  lmodscad  12784  lmodvscad  12785  ipsbased  12794  ipsaddgd  12795  ipsmulrd  12796  ipsscad  12797  ipsvscad  12798  ipsipd  12799  topgrpbasd  12814  topgrpplusgd  12815  topgrptsetd  12816  mulgnnp1  13200  znf1o  14139  lmconst  14384  lmss  14414  uptx  14442  cnmpt1res  14464  dvidlemap  14845  dvrecap  14862  pilem3  14918  logbleb  15093  logblt  15094  lgseisenlem1  15186  djulclALT  15293  djurclALT  15294  pwle2  15489  trilpolemeq1  15530