Theorem eleqtrdi 2233

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  eleqtrrdi  2234  prid2g  3636  freccllem  6307  finomni  7020  exmidomniim  7021  ismkvnex  7037  exmidaclem  7081  caucvgprprlem2  7542  gt0srpr  7580  eluzel2  9355  fseq1p1m1  9905  fznn0sub2  9936  nn0split  9944  nnsplit  9945  exple1  10380  bcval5  10541  bcpasc  10544  zfz1isolemsplit  10613  seq3coll  10617  clim2ser  11138  clim2ser2  11139  iserex  11140  isermulc2  11141  iserle  11143  iserge0  11144  climub  11145  climserle  11146  serf0  11153  summodclem3  11181  summodclem2a  11182  fsum3  11188  sum0  11189  fsumcl2lem  11199  fsumadd  11207  isumclim3  11224  isumadd  11232  fsump1i  11234  fsummulc2  11249  cvgcmpub  11277  binom1dif  11288  isumshft  11291  isumsplit  11292  isumrpcl  11295  arisum2  11300  trireciplem  11301  geoserap  11308  geolim  11312  geo2lim  11317  cvgratnnlemnexp  11325  cvgratnnlemseq  11327  cvgratgt0  11334  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2prod  11340  clim2divap  11341  prodmodclem3  11376  prodmodclem2a  11377  fprodseq  11384  efcvgfsum  11410  efcj  11416  effsumlt  11435  mod2eq1n2dvds  11612  algrp1  11763  phiprmpw  11934  crth  11936  phimullem  11937  ennnfonelemp1  11955  istps  12238  topontopn  12243  cldrcl  12310  cnrehmeocntop  12801  nnsf  13374  nninfsellemqall  13386  nninfomnilem  13389  cvgcmp2nlemabs  13402  trilpolemeq1  13408