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

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

This theorem is referenced by:  brelrng  4969  elabrex  5908  elabrexg  5909  fliftel1  5945  ovidig  6149  unielxp  6346  2oconcl  6650  ecopqsi  6802  eroprf  6840  exmidpweq  7144  sbthlem2  7200  djulclr  7308  djurclr  7309  djulcl  7310  djurcl  7311  caseinl  7350  caseinr  7351  ctssdccl  7370  isnumi  7446  addclnq  7655  mulclnq  7656  recexnq  7670  ltexnqq  7688  prarloclemarch  7698  prarloclemarch2  7699  nnnq  7702  nqnq0  7721  addclnq0  7731  mulclnq0  7732  nqpnq0nq  7733  prarloclemlt  7773  prarloclemlo  7774  prarloclemcalc  7782  nqprm  7822  cauappcvgprlem2  7940  caucvgprlem2  7960  addclsr  8033  mulclsr  8034  prsrcl  8064  mappsrprg  8084  suplocsrlemb  8086  pitonnlem2  8127  pitore  8130  recnnre  8131  axaddcl  8144  axmulcl  8146  axcaucvglemcl  8175  axcaucvglemval  8177  axcaucvglemcau  8178  axcaucvglemres  8179  uztrn2  9835  eluz2nn  9861  peano2uzs  9879  rebtwn2z  10577  seqf  10789  ser0  10858  bcm1k  11085  bcp1nk  11087  bcpasc  11091  hashennn  11105  hashcl  11106  climconst  11930  climshft2  11946  clim2ser  11977  clim2ser2  11978  iserex  11979  serf0  11992  zsumdc  12025  fsump1i  12074  iserabs  12116  isumshft  12131  isumsplit  12132  isum1p  12133  isumrpcl  12135  cvgratnnlemseq  12167  cvgratz  12173  cvgratgt0  12174  clim2prod  12180  clim2divap  12181  prodf1  12183  ntrivcvgap0  12190  zproddc  12220  fprodntrivap  12225  fprodabs  12257  fprodeq0  12258  ef0lem  12301  dvdsflip  12492  fzo0dvdseq  12498  bitsinv1  12603  gcdsupcl  12609  nninfctlemfo  12691  ialgr0  12696  prmind2  12772  crth  12876  prmdiv  12887  pockthlem  13009  pockthg  13010  prmunb  13015  ennnfonelemkh  13113  ennnfonelemrn  13120  ennnfonelemdm  13121  ctiunctlemf  13139  strslfv2d  13205  bassetsnn  13219  1strbas  13280  2strbasg  13283  2stropg  13284  2strbas1g  13286  rngbaseg  13299  rngplusgg  13300  rngmulrg  13301  srngbased  13310  srngplusgd  13311  srngmulrd  13312  srnginvld  13313  lmodbased  13328  lmodplusgd  13329  lmodscad  13330  lmodvscad  13331  ipsbased  13340  ipsaddgd  13341  ipsmulrd  13342  ipsscad  13343  ipsvscad  13344  ipsipd  13345  topgrpbasd  13360  topgrpplusgd  13361  topgrptsetd  13362  mulgnnp1  13797  znf1o  14747  lmconst  15027  lmss  15057  uptx  15085  cnmpt1res  15107  dvidlemap  15502  dvidrelem  15503  dvrecap  15524  plycolemc  15569  plycn  15573  pilem3  15594  logbleb  15772  logblt  15773  lgseisenlem1  15889  structvtxval  15980  ushgredgedgloop  16169  subgruhgredgdm  16211  wlkvtxm  16281  wlk1walkdom  16300  depindlem2  16448  djulclALT  16519  djurclALT  16520  pwle2  16720  trilpolemeq1  16772