Theorem eleqtrrdi 2326

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  brelrng  4988  elabrex  5930  elabrexg  5931  fliftel1  5967  ovidig  6171  unielxp  6368  2oconcl  6672  ecopqsi  6824  eroprf  6862  exmidpweq  7169  sbthlem2  7228  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  caseinl  7382  caseinr  7383  ctssdccl  7402  isnumi  7478  addclnq  7690  mulclnq  7691  recexnq  7705  ltexnqq  7723  prarloclemarch  7733  prarloclemarch2  7734  nnnq  7737  nqnq0  7756  addclnq0  7766  mulclnq0  7767  nqpnq0nq  7768  prarloclemlt  7808  prarloclemlo  7809  prarloclemcalc  7817  nqprm  7857  cauappcvgprlem2  7975  caucvgprlem2  7995  addclsr  8068  mulclsr  8069  prsrcl  8099  mappsrprg  8119  suplocsrlemb  8121  pitonnlem2  8162  pitore  8165  recnnre  8166  axaddcl  8179  axmulcl  8181  axcaucvglemcl  8210  axcaucvglemval  8212  axcaucvglemcau  8213  axcaucvglemres  8214  uztrn2  9872  eluz2nn  9898  peano2uzs  9916  rebtwn2z  10614  seqf  10826  ser0  10895  bcm1k  11122  bcp1nk  11124  bcpasc  11128  hashennn  11143  hashcl  11144  climconst  11975  climshft2  11991  clim2ser  12022  clim2ser2  12023  iserex  12024  serf0  12037  zsumdc  12070  fsump1i  12119  iserabs  12161  isumshft  12176  isumsplit  12177  isum1p  12178  isumrpcl  12180  cvgratnnlemseq  12212  cvgratz  12218  cvgratgt0  12219  clim2prod  12225  clim2divap  12226  prodf1  12228  ntrivcvgap0  12235  zproddc  12265  fprodntrivap  12270  fprodabs  12302  fprodeq0  12303  ef0lem  12346  dvdsflip  12537  fzo0dvdseq  12543  bitsinv1  12648  gcdsupcl  12654  nninfctlemfo  12736  ialgr0  12741  prmind2  12817  crth  12921  prmdiv  12932  pockthlem  13054  pockthg  13055  prmunb  13060  ennnfonelemkh  13163  ennnfonelemrn  13170  ennnfonelemdm  13171  ctiunctlemf  13189  strslfv2d  13255  bassetsnn  13269  1strbas  13330  2strbasg  13333  2stropg  13334  2strbas1g  13336  rngbaseg  13349  rngplusgg  13350  rngmulrg  13351  srngbased  13360  srngplusgd  13361  srngmulrd  13362  srnginvld  13363  lmodbased  13378  lmodplusgd  13379  lmodscad  13380  lmodvscad  13381  ipsbased  13390  ipsaddgd  13391  ipsmulrd  13392  ipsscad  13393  ipsvscad  13394  ipsipd  13395  topgrpbasd  13410  topgrpplusgd  13411  topgrptsetd  13412  mulgnnp1  13847  znf1o  14799  lmconst  15081  lmss  15111  uptx  15139  cnmpt1res  15161  dvidlemap  15556  dvidrelem  15557  dvrecap  15578  plycolemc  15623  plycn  15627  pilem3  15648  logbleb  15826  logblt  15827  lgseisenlem1  15943  structvtxval  16034  ushgredgedgloop  16223  subgruhgredgdm  16265  wlkvtxm  16335  wlk1walkdom  16354  depindlem2  16502  djulclALT  16573  djurclALT  16574  pwle2  16772  trilpolemeq1  16824