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  5881  elabrexg  5882  fliftel1  5918  ovidig  6122  unielxp  6320  2oconcl  6585  ecopqsi  6737  eroprf  6775  exmidpweq  7071  sbthlem2  7125  djulclr  7216  djurclr  7217  djulcl  7218  djurcl  7219  caseinl  7258  caseinr  7259  ctssdccl  7278  isnumi  7354  addclnq  7562  mulclnq  7563  recexnq  7577  ltexnqq  7595  prarloclemarch  7605  prarloclemarch2  7606  nnnq  7609  nqnq0  7628  addclnq0  7638  mulclnq0  7639  nqpnq0nq  7640  prarloclemlt  7680  prarloclemlo  7681  prarloclemcalc  7689  nqprm  7729  cauappcvgprlem2  7847  caucvgprlem2  7867  addclsr  7940  mulclsr  7941  prsrcl  7971  mappsrprg  7991  suplocsrlemb  7993  pitonnlem2  8034  pitore  8037  recnnre  8038  axaddcl  8051  axmulcl  8053  axcaucvglemcl  8082  axcaucvglemval  8084  axcaucvglemcau  8085  axcaucvglemres  8086  uztrn2  9740  eluz2nn  9761  peano2uzs  9779  rebtwn2z  10474  seqf  10686  ser0  10755  bcm1k  10982  bcp1nk  10984  bcpasc  10988  hashennn  11002  hashcl  11003  climconst  11801  climshft2  11817  clim2ser  11848  clim2ser2  11849  iserex  11850  serf0  11863  zsumdc  11895  fsump1i  11944  iserabs  11986  isumshft  12001  isumsplit  12002  isum1p  12003  isumrpcl  12005  cvgratnnlemseq  12037  cvgratz  12043  cvgratgt0  12044  clim2prod  12050  clim2divap  12051  prodf1  12053  ntrivcvgap0  12060  zproddc  12090  fprodntrivap  12095  fprodabs  12127  fprodeq0  12128  ef0lem  12171  dvdsflip  12362  fzo0dvdseq  12368  bitsinv1  12473  gcdsupcl  12479  nninfctlemfo  12561  ialgr0  12566  prmind2  12642  crth  12746  prmdiv  12757  pockthlem  12879  pockthg  12880  prmunb  12885  ennnfonelemkh  12983  ennnfonelemrn  12990  ennnfonelemdm  12991  ctiunctlemf  13009  strslfv2d  13075  bassetsnn  13089  1strbas  13150  2strbasg  13153  2stropg  13154  2strbas1g  13156  rngbaseg  13169  rngplusgg  13170  rngmulrg  13171  srngbased  13180  srngplusgd  13181  srngmulrd  13182  srnginvld  13183  lmodbased  13198  lmodplusgd  13199  lmodscad  13200  lmodvscad  13201  ipsbased  13210  ipsaddgd  13211  ipsmulrd  13212  ipsscad  13213  ipsvscad  13214  ipsipd  13215  topgrpbasd  13230  topgrpplusgd  13231  topgrptsetd  13232  mulgnnp1  13667  znf1o  14615  lmconst  14890  lmss  14920  uptx  14948  cnmpt1res  14970  dvidlemap  15365  dvidrelem  15366  dvrecap  15387  plycolemc  15432  plycn  15436  pilem3  15457  logbleb  15635  logblt  15636  lgseisenlem1  15749  structvtxval  15840  ushgredgedgloop  16026  wlk1walkdom  16070  djulclALT  16165  djurclALT  16166  pwle2  16364  trilpolemeq1  16408