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  7079  sbthlem2  7133  djulclr  7224  djurclr  7225  djulcl  7226  djurcl  7227  caseinl  7266  caseinr  7267  ctssdccl  7286  isnumi  7362  addclnq  7570  mulclnq  7571  recexnq  7585  ltexnqq  7603  prarloclemarch  7613  prarloclemarch2  7614  nnnq  7617  nqnq0  7636  addclnq0  7646  mulclnq0  7647  nqpnq0nq  7648  prarloclemlt  7688  prarloclemlo  7689  prarloclemcalc  7697  nqprm  7737  cauappcvgprlem2  7855  caucvgprlem2  7875  addclsr  7948  mulclsr  7949  prsrcl  7979  mappsrprg  7999  suplocsrlemb  8001  pitonnlem2  8042  pitore  8045  recnnre  8046  axaddcl  8059  axmulcl  8061  axcaucvglemcl  8090  axcaucvglemval  8092  axcaucvglemcau  8093  axcaucvglemres  8094  uztrn2  9748  eluz2nn  9769  peano2uzs  9787  rebtwn2z  10482  seqf  10694  ser0  10763  bcm1k  10990  bcp1nk  10992  bcpasc  10996  hashennn  11010  hashcl  11011  climconst  11809  climshft2  11825  clim2ser  11856  clim2ser2  11857  iserex  11858  serf0  11871  zsumdc  11903  fsump1i  11952  iserabs  11994  isumshft  12009  isumsplit  12010  isum1p  12011  isumrpcl  12013  cvgratnnlemseq  12045  cvgratz  12051  cvgratgt0  12052  clim2prod  12058  clim2divap  12059  prodf1  12061  ntrivcvgap0  12068  zproddc  12098  fprodntrivap  12103  fprodabs  12135  fprodeq0  12136  ef0lem  12179  dvdsflip  12370  fzo0dvdseq  12376  bitsinv1  12481  gcdsupcl  12487  nninfctlemfo  12569  ialgr0  12574  prmind2  12650  crth  12754  prmdiv  12765  pockthlem  12887  pockthg  12888  prmunb  12893  ennnfonelemkh  12991  ennnfonelemrn  12998  ennnfonelemdm  12999  ctiunctlemf  13017  strslfv2d  13083  bassetsnn  13097  1strbas  13158  2strbasg  13161  2stropg  13162  2strbas1g  13164  rngbaseg  13177  rngplusgg  13178  rngmulrg  13179  srngbased  13188  srngplusgd  13189  srngmulrd  13190  srnginvld  13191  lmodbased  13206  lmodplusgd  13207  lmodscad  13208  lmodvscad  13209  ipsbased  13218  ipsaddgd  13219  ipsmulrd  13220  ipsscad  13221  ipsvscad  13222  ipsipd  13223  topgrpbasd  13238  topgrpplusgd  13239  topgrptsetd  13240  mulgnnp1  13675  znf1o  14623  lmconst  14898  lmss  14928  uptx  14956  cnmpt1res  14978  dvidlemap  15373  dvidrelem  15374  dvrecap  15395  plycolemc  15440  plycn  15444  pilem3  15465  logbleb  15643  logblt  15644  lgseisenlem1  15757  structvtxval  15848  ushgredgedgloop  16034  wlkvtxm  16061  wlk1walkdom  16080  djulclALT  16189  djurclALT  16190  pwle2  16390  trilpolemeq1  16435