Theorem eleqtrdi 2298

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleqtrrdi  2299  prid2g  3738  freccllem  6490  nninfisol  7237  finomni  7244  exmidomniim  7245  ismkvnex  7259  exmidaclem  7322  caucvgprprlem2  7825  gt0srpr  7863  eluzel2  9655  fseq1p1m1  10218  fznn0sub2  10252  nn0split  10260  nnsplit  10261  exple1  10742  bcval5  10910  bcpasc  10913  zfz1isolemsplit  10985  seq3coll  10989  ccatrn  11068  swrdccat2  11127  clim2ser  11681  clim2ser2  11682  iserex  11683  isermulc2  11684  iserle  11686  iserge0  11687  climub  11688  climserle  11689  serf0  11696  summodclem3  11724  summodclem2a  11725  fsum3  11731  sum0  11732  fsumcl2lem  11742  fsumadd  11750  isumclim3  11767  isumadd  11775  fsump1i  11777  fsummulc2  11792  cvgcmpub  11820  binom1dif  11831  isumshft  11834  isumsplit  11835  isumrpcl  11838  arisum2  11843  trireciplem  11844  geoserap  11851  geolim  11855  geo2lim  11860  cvgratnnlemnexp  11868  cvgratnnlemseq  11870  cvgratgt0  11877  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  clim2prod  11883  clim2divap  11884  prodmodclem3  11919  prodmodclem2a  11920  fprodseq  11927  fprodntrivap  11928  fprodssdc  11934  fprodmul  11935  fprodabs  11960  fprodeq0  11961  efcvgfsum  12011  efcj  12017  effsumlt  12036  mod2eq1n2dvds  12223  bitsfzolem  12298  bitsfzo  12299  bitsfi  12301  bitsinv1lem  12305  bitsinv1  12306  nninfctlemfo  12394  algrp1  12401  phiprmpw  12577  crth  12579  phimullem  12580  prmdiv  12590  pcpremul  12649  pcmpt  12699  pcfac  12706  pockthlem  12712  pockthg  12713  1arith  12723  ennnfonelemp1  12810  nninfdclemp1  12854  relelbasov  12927  gsumwsubmcl  13361  gsumwmhm  13363  mulgnnp1  13499  mulgnn0z  13518  mulgnndir  13520  idomdomd  14072  idomcringd  14073  lspprid2  14207  istps  14537  topontopn  14542  cldrcl  14607  cnrehmeocntop  15115  elplyd  15246  ply1termlem  15247  ply1term  15248  plyaddlem1  15252  plymullem1  15253  plyaddlem  15254  plymullem  15255  plycoeid3  15262  plycolemc  15263  plycj  15266  dvply1  15270  0sgmppw  15498  1sgmprm  15499  lgsval2lem  15520  lgsdir2lem3  15540  lgsdir2lem5  15542  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  gausslemma2dlem3  15573  lgseisenlem1  15580  lgseisenlem4  15583  lgsquadlem2  15588  2omap  15969  nnsf  15979  nninfsellemqall  15989  nninfomnilem  15992  nnnninfex  15996  nninfnfiinf  15997  cvgcmp2nlemabs  16008  trilpolemeq1  16016  nconstwlpolemgt0  16040