Theorem eleqtrdi 2263

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 2249	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleqtrrdi  2264  prid2g  3686  freccllem  6378  nninfisol  7105  finomni  7112  exmidomniim  7113  ismkvnex  7127  exmidaclem  7172  caucvgprprlem2  7659  gt0srpr  7697  eluzel2  9479  fseq1p1m1  10037  fznn0sub2  10071  nn0split  10079  nnsplit  10080  exple1  10519  bcval5  10684  bcpasc  10687  zfz1isolemsplit  10760  seq3coll  10764  clim2ser  11287  clim2ser2  11288  iserex  11289  isermulc2  11290  iserle  11292  iserge0  11293  climub  11294  climserle  11295  serf0  11302  summodclem3  11330  summodclem2a  11331  fsum3  11337  sum0  11338  fsumcl2lem  11348  fsumadd  11356  isumclim3  11373  isumadd  11381  fsump1i  11383  fsummulc2  11398  cvgcmpub  11426  binom1dif  11437  isumshft  11440  isumsplit  11441  isumrpcl  11444  arisum2  11449  trireciplem  11450  geoserap  11457  geolim  11461  geo2lim  11466  cvgratnnlemnexp  11474  cvgratnnlemseq  11476  cvgratgt0  11483  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  clim2prod  11489  clim2divap  11490  prodmodclem3  11525  prodmodclem2a  11526  fprodseq  11533  fprodntrivap  11534  fprodssdc  11540  fprodmul  11541  fprodabs  11566  fprodeq0  11567  efcvgfsum  11617  efcj  11623  effsumlt  11642  mod2eq1n2dvds  11825  algrp1  11987  phiprmpw  12163  crth  12165  phimullem  12166  prmdiv  12176  pcpremul  12234  pcmpt  12282  pcfac  12289  pockthlem  12295  pockthg  12296  1arith  12306  ennnfonelemp1  12348  nninfdclemp1  12392  istps  12783  topontopn  12788  cldrcl  12855  cnrehmeocntop  13346  lgsval2lem  13664  lgsdir2lem3  13684  lgsdir2lem5  13686  lgsdir  13689  lgsdilem2  13690  lgsdi  13691  lgsne0  13692  nnsf  13998  nninfsellemqall  14008  nninfomnilem  14011  cvgcmp2nlemabs  14024  trilpolemeq1  14032  nconstwlpolemgt0  14055