Theorem eleqtrdi 2258

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eleqtrdi.1	|- ( ph -> A e. B )
eleqtrdi.2	|- B = C

Assertion

Ref	Expression
eleqtrdi	|- ( ph -> A e. C )

Proof of Theorem eleqtrdi

Step	Hyp	Ref	Expression
1		eleqtrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrdi.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2244	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleqtrrdi  2259  prid2g  3680  freccllem  6366  nninfisol  7093  finomni  7100  exmidomniim  7101  ismkvnex  7115  exmidaclem  7160  caucvgprprlem2  7647  gt0srpr  7685  eluzel2  9467  fseq1p1m1  10025  fznn0sub2  10059  nn0split  10067  nnsplit  10068  exple1  10507  bcval5  10672  bcpasc  10675  zfz1isolemsplit  10747  seq3coll  10751  clim2ser  11274  clim2ser2  11275  iserex  11276  isermulc2  11277  iserle  11279  iserge0  11280  climub  11281  climserle  11282  serf0  11289  summodclem3  11317  summodclem2a  11318  fsum3  11324  sum0  11325  fsumcl2lem  11335  fsumadd  11343  isumclim3  11360  isumadd  11368  fsump1i  11370  fsummulc2  11385  cvgcmpub  11413  binom1dif  11424  isumshft  11427  isumsplit  11428  isumrpcl  11431  arisum2  11436  trireciplem  11437  geoserap  11444  geolim  11448  geo2lim  11453  cvgratnnlemnexp  11461  cvgratnnlemseq  11463  cvgratgt0  11470  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  clim2prod  11476  clim2divap  11477  prodmodclem3  11512  prodmodclem2a  11513  fprodseq  11520  fprodntrivap  11521  fprodssdc  11527  fprodmul  11528  fprodabs  11553  fprodeq0  11554  efcvgfsum  11604  efcj  11610  effsumlt  11629  mod2eq1n2dvds  11812  algrp1  11974  phiprmpw  12150  crth  12152  phimullem  12153  prmdiv  12163  pcpremul  12221  pcmpt  12269  pcfac  12276  pockthlem  12282  pockthg  12283  1arith  12293  ennnfonelemp1  12335  nninfdclemp1  12379  istps  12630  topontopn  12635  cldrcl  12702  cnrehmeocntop  13193  lgsval2lem  13511  lgsdir2lem3  13531  lgsdir2lem5  13533  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  nnsf  13845  nninfsellemqall  13855  nninfomnilem  13858  cvgcmp2nlemabs  13871  trilpolemeq1  13879  nconstwlpolemgt0  13902