Theorem eleqtrrdi 2328

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  brelrng  4993  elabrex  5936  elabrexg  5937  fliftel1  5973  ovidig  6179  unielxp  6381  2oconcl  6685  ecopqsi  6837  eroprf  6875  exmidpweq  7182  sbthlem2  7241  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  caseinl  7395  caseinr  7396  ctssdccl  7415  isnumi  7491  addclnq  7706  mulclnq  7707  recexnq  7721  ltexnqq  7739  prarloclemarch  7749  prarloclemarch2  7750  nnnq  7753  nqnq0  7772  addclnq0  7782  mulclnq0  7783  nqpnq0nq  7784  prarloclemlt  7824  prarloclemlo  7825  prarloclemcalc  7833  nqprm  7873  cauappcvgprlem2  7991  caucvgprlem2  8011  addclsr  8084  mulclsr  8085  prsrcl  8115  mappsrprg  8135  suplocsrlemb  8137  pitonnlem2  8178  pitore  8181  recnnre  8182  axaddcl  8195  axmulcl  8197  axcaucvglemcl  8226  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  uztrn2  9890  eluz2nn  9916  peano2uzs  9934  rebtwn2z  10638  seqf  10850  ser0  10919  bcm1k  11147  bcp1nk  11149  bcpasc  11153  hashennn  11168  hashcl  11169  climconst  12000  climshft2  12016  clim2ser  12047  clim2ser2  12048  iserex  12049  serf0  12062  zsumdc  12095  fsump1i  12144  iserabs  12186  isumshft  12201  isumsplit  12202  isum1p  12203  isumrpcl  12205  cvgratnnlemseq  12237  cvgratz  12243  cvgratgt0  12244  clim2prod  12250  clim2divap  12251  prodf1  12253  ntrivcvgap0  12260  zproddc  12290  fprodntrivap  12295  fprodabs  12327  fprodeq0  12328  ef0lem  12371  dvdsflip  12562  fzo0dvdseq  12568  bitsinv1  12673  gcdsupcl  12679  nninfctlemfo  12761  ialgr0  12766  prmind2  12842  crth  12946  prmdiv  12957  pockthlem  13079  pockthg  13080  prmunb  13085  ennnfonelemkh  13247  ennnfonelemrn  13254  ennnfonelemdm  13255  ctiunctlemf  13273  strslfv2d  13339  bassetsnn  13353  1strbas  13414  2strbasg  13417  2stropg  13418  2strbas1g  13420  rngbaseg  13433  rngplusgg  13434  rngmulrg  13435  srngbased  13444  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodbased  13462  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsbased  13474  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  topgrpbasd  13494  topgrpplusgd  13495  topgrptsetd  13496  mulgnnp1  13883  znf1o  14925  lmconst  15207  lmss  15237  uptx  15265  cnmpt1res  15287  dvidlemap  15682  dvidrelem  15683  dvrecap  15704  plycolemc  15749  plycn  15753  pilem3  15774  logbleb  15952  logblt  15953  lgseisenlem1  16069  structvtxval  16160  ushgredgedgloop  16349  subgruhgredgdm  16391  wlkvtxm  16461  wlk1walkdom  16480  depindlem2  16628  djulclALT  16699  djurclALT  16700  pwle2  16898  trilpolemeq1  16950