Theorem eleqtrrdi 2271

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  brelrng  4855  elabrex  5754  fliftel1  5790  ovidig  5987  unielxp  6170  2oconcl  6435  ecopqsi  6585  eroprf  6623  exmidpweq  6904  sbthlem2  6952  djulclr  7043  djurclr  7044  djulcl  7045  djurcl  7046  caseinl  7085  caseinr  7086  ctssdccl  7105  isnumi  7176  addclnq  7369  mulclnq  7370  recexnq  7384  ltexnqq  7402  prarloclemarch  7412  prarloclemarch2  7413  nnnq  7416  nqnq0  7435  addclnq0  7445  mulclnq0  7446  nqpnq0nq  7447  prarloclemlt  7487  prarloclemlo  7488  prarloclemcalc  7496  nqprm  7536  cauappcvgprlem2  7654  caucvgprlem2  7674  addclsr  7747  mulclsr  7748  prsrcl  7778  mappsrprg  7798  suplocsrlemb  7800  pitonnlem2  7841  pitore  7844  recnnre  7845  axaddcl  7858  axmulcl  7860  axcaucvglemcl  7889  axcaucvglemval  7891  axcaucvglemcau  7892  axcaucvglemres  7893  uztrn2  9539  eluz2nn  9560  peano2uzs  9578  rebtwn2z  10248  seqf  10454  ser0  10507  bcm1k  10731  bcp1nk  10733  bcpasc  10737  hashennn  10751  hashcl  10752  climconst  11289  climshft2  11305  clim2ser  11336  clim2ser2  11337  iserex  11338  serf0  11351  zsumdc  11383  fsump1i  11432  iserabs  11474  isumshft  11489  isumsplit  11490  isum1p  11491  isumrpcl  11493  cvgratnnlemseq  11525  cvgratz  11531  cvgratgt0  11532  clim2prod  11538  clim2divap  11539  prodf1  11541  ntrivcvgap0  11548  zproddc  11578  fprodntrivap  11583  fprodabs  11615  fprodeq0  11616  ef0lem  11659  dvdsflip  11847  fzo0dvdseq  11853  gcdsupcl  11949  ialgr0  12034  prmind2  12110  crth  12214  prmdiv  12225  pockthlem  12344  pockthg  12345  prmunb  12350  ennnfonelemkh  12403  ennnfonelemrn  12410  ennnfonelemdm  12411  ctiunctlemf  12429  strslfv2d  12495  1strbas  12566  2strbasg  12568  2stropg  12569  2strbas1g  12571  rngbaseg  12584  rngplusgg  12585  rngmulrg  12586  srngbased  12595  srngplusgd  12596  srngmulrd  12597  srnginvld  12598  lmodbased  12613  lmodplusgd  12614  lmodscad  12615  lmodvscad  12616  ipsbased  12625  ipsaddgd  12626  ipsmulrd  12627  ipsscad  12628  ipsvscad  12629  ipsipd  12630  topgrpbasd  12642  topgrpplusgd  12643  topgrptsetd  12644  mulgnnp1  12919  lmconst  13498  lmss  13528  uptx  13556  cnmpt1res  13578  dvidlemap  13942  dvrecap  13959  pilem3  13986  logbleb  14161  logblt  14162  djulclALT  14324  djurclALT  14325  pwle2  14519  trilpolemeq1  14559