Theorem eleqtrrdi 2325

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  brelrng  4963  elabrex  5898  elabrexg  5899  fliftel1  5935  ovidig  6139  unielxp  6337  2oconcl  6607  ecopqsi  6759  eroprf  6797  exmidpweq  7101  sbthlem2  7157  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  caseinl  7290  caseinr  7291  ctssdccl  7310  isnumi  7386  addclnq  7595  mulclnq  7596  recexnq  7610  ltexnqq  7628  prarloclemarch  7638  prarloclemarch2  7639  nnnq  7642  nqnq0  7661  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  prarloclemlt  7713  prarloclemlo  7714  prarloclemcalc  7722  nqprm  7762  cauappcvgprlem2  7880  caucvgprlem2  7900  addclsr  7973  mulclsr  7974  prsrcl  8004  mappsrprg  8024  suplocsrlemb  8026  pitonnlem2  8067  pitore  8070  recnnre  8071  axaddcl  8084  axmulcl  8086  axcaucvglemcl  8115  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  uztrn2  9774  eluz2nn  9800  peano2uzs  9818  rebtwn2z  10515  seqf  10727  ser0  10796  bcm1k  11023  bcp1nk  11025  bcpasc  11029  hashennn  11043  hashcl  11044  climconst  11868  climshft2  11884  clim2ser  11915  clim2ser2  11916  iserex  11917  serf0  11930  zsumdc  11963  fsump1i  12012  iserabs  12054  isumshft  12069  isumsplit  12070  isum1p  12071  isumrpcl  12073  cvgratnnlemseq  12105  cvgratz  12111  cvgratgt0  12112  clim2prod  12118  clim2divap  12119  prodf1  12121  ntrivcvgap0  12128  zproddc  12158  fprodntrivap  12163  fprodabs  12195  fprodeq0  12196  ef0lem  12239  dvdsflip  12430  fzo0dvdseq  12436  bitsinv1  12541  gcdsupcl  12547  nninfctlemfo  12629  ialgr0  12634  prmind2  12710  crth  12814  prmdiv  12825  pockthlem  12947  pockthg  12948  prmunb  12953  ennnfonelemkh  13051  ennnfonelemrn  13058  ennnfonelemdm  13059  ctiunctlemf  13077  strslfv2d  13143  bassetsnn  13157  1strbas  13218  2strbasg  13221  2stropg  13222  2strbas1g  13224  rngbaseg  13237  rngplusgg  13238  rngmulrg  13239  srngbased  13248  srngplusgd  13249  srngmulrd  13250  srnginvld  13251  lmodbased  13266  lmodplusgd  13267  lmodscad  13268  lmodvscad  13269  ipsbased  13278  ipsaddgd  13279  ipsmulrd  13280  ipsscad  13281  ipsvscad  13282  ipsipd  13283  topgrpbasd  13298  topgrpplusgd  13299  topgrptsetd  13300  mulgnnp1  13735  znf1o  14684  lmconst  14959  lmss  14989  uptx  15017  cnmpt1res  15039  dvidlemap  15434  dvidrelem  15435  dvrecap  15456  plycolemc  15501  plycn  15505  pilem3  15526  logbleb  15704  logblt  15705  lgseisenlem1  15818  structvtxval  15909  ushgredgedgloop  16098  subgruhgredgdm  16140  wlkvtxm  16210  wlk1walkdom  16229  depindlem2  16377  djulclALT  16448  djurclALT  16449  pwle2  16650  trilpolemeq1  16695