Theorem eleqtrdi 2270

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 2256	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:  eleqtrrdi  2271  prid2g  3699  freccllem  6405  nninfisol  7133  finomni  7140  exmidomniim  7141  ismkvnex  7155  exmidaclem  7209  caucvgprprlem2  7711  gt0srpr  7749  eluzel2  9535  fseq1p1m1  10096  fznn0sub2  10130  nn0split  10138  nnsplit  10139  exple1  10578  bcval5  10745  bcpasc  10748  zfz1isolemsplit  10820  seq3coll  10824  clim2ser  11347  clim2ser2  11348  iserex  11349  isermulc2  11350  iserle  11352  iserge0  11353  climub  11354  climserle  11355  serf0  11362  summodclem3  11390  summodclem2a  11391  fsum3  11397  sum0  11398  fsumcl2lem  11408  fsumadd  11416  isumclim3  11433  isumadd  11441  fsump1i  11443  fsummulc2  11458  cvgcmpub  11486  binom1dif  11497  isumshft  11500  isumsplit  11501  isumrpcl  11504  arisum2  11509  trireciplem  11510  geoserap  11517  geolim  11521  geo2lim  11526  cvgratnnlemnexp  11534  cvgratnnlemseq  11536  cvgratgt0  11543  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  clim2prod  11549  clim2divap  11550  prodmodclem3  11585  prodmodclem2a  11586  fprodseq  11593  fprodntrivap  11594  fprodssdc  11600  fprodmul  11601  fprodabs  11626  fprodeq0  11627  efcvgfsum  11677  efcj  11683  effsumlt  11702  mod2eq1n2dvds  11886  algrp1  12048  phiprmpw  12224  crth  12226  phimullem  12227  prmdiv  12237  pcpremul  12295  pcmpt  12343  pcfac  12350  pockthlem  12356  pockthg  12357  1arith  12367  ennnfonelemp1  12409  nninfdclemp1  12453  mulgnnp1  12996  mulgnn0z  13015  mulgnndir  13017  lspprid2  13503  istps  13617  topontopn  13622  cldrcl  13687  cnrehmeocntop  14178  lgsval2lem  14496  lgsdir2lem3  14516  lgsdir2lem5  14518  lgsdir  14521  lgsdilem2  14522  lgsdi  14523  lgsne0  14524  lgseisenlem1  14535  nnsf  14839  nninfsellemqall  14849  nninfomnilem  14852  cvgcmp2nlemabs  14865  trilpolemeq1  14873  nconstwlpolemgt0  14897