Theorem eleqtrdi 2289

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleqtrrdi  2290  prid2g  3728  freccllem  6469  nninfisol  7208  finomni  7215  exmidomniim  7216  ismkvnex  7230  exmidaclem  7291  caucvgprprlem2  7794  gt0srpr  7832  eluzel2  9623  fseq1p1m1  10186  fznn0sub2  10220  nn0split  10228  nnsplit  10229  exple1  10704  bcval5  10872  bcpasc  10875  zfz1isolemsplit  10947  seq3coll  10951  clim2ser  11519  clim2ser2  11520  iserex  11521  isermulc2  11522  iserle  11524  iserge0  11525  climub  11526  climserle  11527  serf0  11534  summodclem3  11562  summodclem2a  11563  fsum3  11569  sum0  11570  fsumcl2lem  11580  fsumadd  11588  isumclim3  11605  isumadd  11613  fsump1i  11615  fsummulc2  11630  cvgcmpub  11658  binom1dif  11669  isumshft  11672  isumsplit  11673  isumrpcl  11676  arisum2  11681  trireciplem  11682  geoserap  11689  geolim  11693  geo2lim  11698  cvgratnnlemnexp  11706  cvgratnnlemseq  11708  cvgratgt0  11715  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  clim2prod  11721  clim2divap  11722  prodmodclem3  11757  prodmodclem2a  11758  fprodseq  11765  fprodntrivap  11766  fprodssdc  11772  fprodmul  11773  fprodabs  11798  fprodeq0  11799  efcvgfsum  11849  efcj  11855  effsumlt  11874  mod2eq1n2dvds  12061  bitsfzolem  12136  bitsfzo  12137  bitsfi  12139  bitsinv1lem  12143  bitsinv1  12144  nninfctlemfo  12232  algrp1  12239  phiprmpw  12415  crth  12417  phimullem  12418  prmdiv  12428  pcpremul  12487  pcmpt  12537  pcfac  12544  pockthlem  12550  pockthg  12551  1arith  12561  ennnfonelemp1  12648  nninfdclemp1  12692  relelbasov  12765  gsumwsubmcl  13198  gsumwmhm  13200  mulgnnp1  13336  mulgnn0z  13355  mulgnndir  13357  idomdomd  13909  idomcringd  13910  lspprid2  14044  istps  14352  topontopn  14357  cldrcl  14422  cnrehmeocntop  14930  elplyd  15061  ply1termlem  15062  ply1term  15063  plyaddlem1  15067  plymullem1  15068  plyaddlem  15069  plymullem  15070  plycoeid3  15077  plycolemc  15078  plycj  15081  dvply1  15085  0sgmppw  15313  1sgmprm  15314  lgsval2lem  15335  lgsdir2lem3  15355  lgsdir2lem5  15357  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  gausslemma2dlem3  15388  lgseisenlem1  15395  lgseisenlem4  15398  lgsquadlem2  15403  2omap  15726  nnsf  15736  nninfsellemqall  15746  nninfomnilem  15749  cvgcmp2nlemabs  15763  trilpolemeq1  15771  nconstwlpolemgt0  15795