Theorem eleqtrrdi 2332

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  brelrng  5013  elabrex  5963  elabrexg  5964  fliftel1  6000  ovidig  6206  unielxp  6408  2oconcl  6712  ecopqsi  6864  eroprf  6902  exmidpweq  7216  sbthlem2  7275  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  caseinl  7431  caseinr  7432  ctssdccl  7451  isnumi  7527  addclnq  7742  mulclnq  7743  recexnq  7757  ltexnqq  7775  prarloclemarch  7785  prarloclemarch2  7786  nnnq  7789  nqnq0  7808  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  prarloclemlt  7860  prarloclemlo  7861  prarloclemcalc  7869  nqprm  7909  cauappcvgprlem2  8027  caucvgprlem2  8047  addclsr  8120  mulclsr  8121  prsrcl  8151  mappsrprg  8171  suplocsrlemb  8173  pitonnlem2  8214  pitore  8217  recnnre  8218  axaddcl  8231  axmulcl  8233  axcaucvglemcl  8262  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  uztrn2  9949  eluz2nn  9975  peano2uzs  9993  rebtwn2z  10699  seqf  10914  ser0  10983  bcm1k  11212  bcp1nk  11214  bcpasc  11218  hashennn  11233  hashcl  11234  climconst  12072  climshft2  12088  clim2ser  12119  clim2ser2  12120  iserex  12121  serf0  12134  zsumdc  12167  fsump1i  12216  iserabs  12258  isumshft  12273  isumsplit  12274  isum1p  12275  isumrpcl  12277  cvgratnnlemseq  12309  cvgratz  12315  cvgratgt0  12316  clim2prod  12322  clim2divap  12323  prodf1  12325  ntrivcvgap0  12332  zproddc  12362  fprodntrivap  12367  fprodabs  12399  fprodeq0  12400  ef0lem  12443  dvdsflip  12634  fzo0dvdseq  12640  bitsinv1  12745  gcdsupcl  12751  nninfctlemfo  12833  ialgr0  12838  prmind2  12914  crth  13022  prmdiv  13033  pockthlem  13155  pockthg  13156  prmunb  13161  ennnfonelemkh  13352  ennnfonelemrn  13359  ennnfonelemdm  13360  ctiunctlemf  13378  strslfv2d  13444  bassetsnn  13458  1strbas  13520  2strbasg  13523  2stropg  13524  2strbas1g  13526  rngbaseg  13539  rngplusgg  13540  rngmulrg  13541  srngbased  13550  srngplusgd  13551  srngmulrd  13552  srnginvld  13553  lmodbased  13568  lmodplusgd  13569  lmodscad  13570  lmodvscad  13571  ipsbased  13580  ipsaddgd  13581  ipsmulrd  13582  ipsscad  13583  ipsvscad  13584  ipsipd  13585  topgrpbasd  13600  topgrpplusgd  13601  topgrptsetd  13602  mulgnnp1  13982  znf1o  15035  lmconst  15366  lmss  15396  uptx  15424  cnmpt1res  15446  dvidlemap  15841  dvidrelem  15842  dvrecap  15863  plycolemc  15908  plycn  15912  pilem3  15934  logbleb  16116  logblt  16117  ppiqub  16194  lgseisenlem1  16287  structvtxval  16378  ushgredgedgloop  16567  subgruhgredgdm  16609  wlkvtxm  16679  wlk1walkdom  16698  depindlem2  16846  djulclALT  16927  djurclALT  16928  pwle2  17126  trilpolemeq1  17187