Theorem eleqtrdi 2322

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  eleqtrrdi  2323  prid2g  3774  freccllem  6563  nninfisol  7323  finomni  7330  exmidomniim  7331  ismkvnex  7345  exmidaclem  7413  pw1m  7432  caucvgprprlem2  7920  gt0srpr  7958  eluzel2  9750  fseq1p1m1  10319  fznn0sub2  10353  nn0split  10361  nnsplit  10362  exple1  10847  bcval5  11015  bcpasc  11018  zfz1isolemsplit  11092  seq3coll  11096  ccatrn  11176  swrdccat2  11242  cats1un  11292  pfxccatin12lem3  11303  cats1fvd  11337  clim2ser  11888  clim2ser2  11889  iserex  11890  isermulc2  11891  iserle  11893  iserge0  11894  climub  11895  climserle  11896  serf0  11903  summodclem3  11931  summodclem2a  11932  fsum3  11938  sum0  11939  fsumcl2lem  11949  fsumadd  11957  isumclim3  11974  isumadd  11982  fsump1i  11984  fsummulc2  11999  cvgcmpub  12027  binom1dif  12038  isumshft  12041  isumsplit  12042  isumrpcl  12045  arisum2  12050  trireciplem  12051  geoserap  12058  geolim  12062  geo2lim  12067  cvgratnnlemnexp  12075  cvgratnnlemseq  12077  cvgratgt0  12084  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  clim2prod  12090  clim2divap  12091  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodntrivap  12135  fprodssdc  12141  fprodmul  12142  fprodabs  12167  fprodeq0  12168  efcvgfsum  12218  efcj  12224  effsumlt  12243  mod2eq1n2dvds  12430  bitsfzolem  12505  bitsfzo  12506  bitsfi  12508  bitsinv1lem  12512  bitsinv1  12513  nninfctlemfo  12601  algrp1  12608  phiprmpw  12784  crth  12786  phimullem  12787  prmdiv  12797  pcpremul  12856  pcmpt  12906  pcfac  12913  pockthlem  12919  pockthg  12920  1arith  12930  ennnfonelemp1  13017  nninfdclemp1  13061  relelbasov  13135  gsumwsubmcl  13569  gsumwmhm  13571  mulgnnp1  13707  mulgnn0z  13726  mulgnndir  13728  idomdomd  14281  idomcringd  14282  lspprid2  14416  istps  14746  topontopn  14751  cldrcl  14816  cnrehmeocntop  15324  elplyd  15455  ply1termlem  15456  ply1term  15457  plyaddlem1  15461  plymullem1  15462  plyaddlem  15463  plymullem  15464  plycoeid3  15471  plycolemc  15472  plycj  15475  dvply1  15479  0sgmppw  15707  1sgmprm  15708  lgsval2lem  15729  lgsdir2lem3  15749  lgsdir2lem5  15751  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  gausslemma2dlem3  15782  lgseisenlem1  15789  lgseisenlem4  15792  lgsquadlem2  15797  umgrpredgv  15986  2omap  16530  nnsf  16543  nninfsellemqall  16553  nninfomnilem  16556  nnnninfex  16560  nninfnfiinf  16561  cvgcmp2nlemabs  16572  trilpolemeq1  16580  nconstwlpolemgt0  16604