Theorem eleqtrdi 2325

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eleqtrrdi  2326  prid2g  3796  freccllem  6633  2omap  7269  nninfisol  7424  finomni  7431  exmidomniim  7432  ismkvnex  7446  exmidaclem  7515  pw1m  7534  caucvgprprlem2  8025  gt0srpr  8063  eluzel2  9858  fseq1p1m1  10428  fznn0sub2  10462  nn0split  10470  nnsplit  10471  exple1  10957  bcval5  11125  bcpasc  11128  zfz1isolemsplit  11210  seq3coll  11214  ccatrn  11297  swrdccat2  11363  cats1un  11413  pfxccatin12lem3  11424  cats1fvd  11458  clim2ser  12022  clim2ser2  12023  iserex  12024  isermulc2  12025  iserle  12027  iserge0  12028  climub  12029  climserle  12030  serf0  12037  summodclem3  12066  summodclem2a  12067  fsum3  12073  sum0  12074  fsumcl2lem  12084  fsumadd  12092  isumclim3  12109  isumadd  12117  fsump1i  12119  fsummulc2  12134  cvgcmpub  12162  binom1dif  12173  isumshft  12176  isumsplit  12177  isumrpcl  12180  arisum2  12185  trireciplem  12186  geoserap  12193  geolim  12197  geo2lim  12202  cvgratnnlemnexp  12210  cvgratnnlemseq  12212  cvgratgt0  12219  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  clim2prod  12225  clim2divap  12226  prodmodclem3  12261  prodmodclem2a  12262  fprodseq  12269  fprodntrivap  12270  fprodssdc  12276  fprodmul  12277  fprodabs  12302  fprodeq0  12303  efcvgfsum  12353  efcj  12359  effsumlt  12378  mod2eq1n2dvds  12565  bitsfzolem  12640  bitsfzo  12641  bitsfi  12643  bitsinv1lem  12647  bitsinv1  12648  nninfctlemfo  12736  algrp1  12743  phiprmpw  12919  crth  12921  phimullem  12922  prmdiv  12932  pcpremul  12991  pcmpt  13041  pcfac  13048  pockthlem  13054  pockthg  13055  1arith  13065  ballotfilem2  13142  ennnfonelemp1  13157  nninfdclemp1  13201  relelbasov  13275  gsumwsubmcl  13709  gsumwmhm  13711  mulgnnp1  13847  mulgnn0z  13866  mulgnndir  13868  idomdomd  14423  idomcringd  14424  lspprid2  14560  istps  14897  topontopn  14902  cldrcl  14967  cnrehmeocntop  15475  elplyd  15606  ply1termlem  15607  ply1term  15608  plyaddlem1  15612  plymullem1  15613  plyaddlem  15614  plymullem  15615  plycoeid3  15622  plycolemc  15623  plycj  15626  dvply1  15630  0sgmppw  15861  1sgmprm  15862  lgsval2lem  15883  lgsdir2lem3  15903  lgsdir2lem5  15905  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  gausslemma2dlem3  15936  lgseisenlem1  15943  lgseisenlem4  15946  lgsquadlem2  15951  umgrpredgv  16142  subgruhgredgdm  16265  eupth2lemsfi  16473  depindlem1  16501  nnsf  16783  nninfsellemqall  16793  nninfomnilem  16796  nnnninfex  16800  nninfnfiinf  16801  cvgcmp2nlemabs  16816  trilpolemeq1  16824  nconstwlpolemgt0  16850  gfsump1  16868