Theorem eleqtrrdi 2323

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  brelrng  4955  elabrex  5887  elabrexg  5888  fliftel1  5924  ovidig  6128  unielxp  6326  2oconcl  6593  ecopqsi  6745  eroprf  6783  exmidpweq  7082  sbthlem2  7136  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  caseinl  7269  caseinr  7270  ctssdccl  7289  isnumi  7365  addclnq  7573  mulclnq  7574  recexnq  7588  ltexnqq  7606  prarloclemarch  7616  prarloclemarch2  7617  nnnq  7620  nqnq0  7639  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  prarloclemlt  7691  prarloclemlo  7692  prarloclemcalc  7700  nqprm  7740  cauappcvgprlem2  7858  caucvgprlem2  7878  addclsr  7951  mulclsr  7952  prsrcl  7982  mappsrprg  8002  suplocsrlemb  8004  pitonnlem2  8045  pitore  8048  recnnre  8049  axaddcl  8062  axmulcl  8064  axcaucvglemcl  8093  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  uztrn2  9752  eluz2nn  9773  peano2uzs  9791  rebtwn2z  10486  seqf  10698  ser0  10767  bcm1k  10994  bcp1nk  10996  bcpasc  11000  hashennn  11014  hashcl  11015  climconst  11817  climshft2  11833  clim2ser  11864  clim2ser2  11865  iserex  11866  serf0  11879  zsumdc  11911  fsump1i  11960  iserabs  12002  isumshft  12017  isumsplit  12018  isum1p  12019  isumrpcl  12021  cvgratnnlemseq  12053  cvgratz  12059  cvgratgt0  12060  clim2prod  12066  clim2divap  12067  prodf1  12069  ntrivcvgap0  12076  zproddc  12106  fprodntrivap  12111  fprodabs  12143  fprodeq0  12144  ef0lem  12187  dvdsflip  12378  fzo0dvdseq  12384  bitsinv1  12489  gcdsupcl  12495  nninfctlemfo  12577  ialgr0  12582  prmind2  12658  crth  12762  prmdiv  12773  pockthlem  12895  pockthg  12896  prmunb  12901  ennnfonelemkh  12999  ennnfonelemrn  13006  ennnfonelemdm  13007  ctiunctlemf  13025  strslfv2d  13091  bassetsnn  13105  1strbas  13166  2strbasg  13169  2stropg  13170  2strbas1g  13172  rngbaseg  13185  rngplusgg  13186  rngmulrg  13187  srngbased  13196  srngplusgd  13197  srngmulrd  13198  srnginvld  13199  lmodbased  13214  lmodplusgd  13215  lmodscad  13216  lmodvscad  13217  ipsbased  13226  ipsaddgd  13227  ipsmulrd  13228  ipsscad  13229  ipsvscad  13230  ipsipd  13231  topgrpbasd  13246  topgrpplusgd  13247  topgrptsetd  13248  mulgnnp1  13683  znf1o  14631  lmconst  14906  lmss  14936  uptx  14964  cnmpt1res  14986  dvidlemap  15381  dvidrelem  15382  dvrecap  15403  plycolemc  15448  plycn  15452  pilem3  15473  logbleb  15651  logblt  15652  lgseisenlem1  15765  structvtxval  15856  ushgredgedgloop  16042  wlkvtxm  16086  wlk1walkdom  16105  djulclALT  16248  djurclALT  16249  pwle2  16451  trilpolemeq1  16496