MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexd Unicode version

Theorem ssexd 4310
Description: A subclass of a set is a set. Deduction form of ssexg 4309. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
ssexd.1  |-  ( ph  ->  B  e.  C )
ssexd.2  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
ssexd  |-  ( ph  ->  A  e.  _V )

Proof of Theorem ssexd
StepHypRef Expression
1 ssexd.2 . 2  |-  ( ph  ->  A  C_  B )
2 ssexd.1 . 2  |-  ( ph  ->  B  e.  C )
3 ssexg 4309 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   _Vcvv 2916    C_ wss 3280
This theorem is referenced by:  soex  5278  fex2  5562  opabbrex  6077  fnwelem  6420  fnse  6422  f1imaen2g  7127  ordtypelem10  7452  oismo  7465  wofib  7470  wemapso  7476  wdom2d  7504  wdomd  7505  unxpwdom2  7512  cantnfle  7582  cantnflt  7583  cantnflt2  7584  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom3lem  7616  acni2  7883  fin1a2lem12  8247  hsmexlem1  8262  zorn2lem4  8335  fpwwe2lem2  8463  fpwwe2lem5  8465  fpwwe2lem12  8472  fpwwe2  8474  fpwwelem  8476  canthwelem  8481  pwfseqlem4  8493  hashbcss  13327  strssd  13458  restid2  13613  divsfval  13727  mrieqv2d  13819  mrissmrcd  13820  mreexexlemd  13824  mreexexlem3d  13826  mreexexlem4d  13827  mreexexd  13828  mreexdomd  13829  rescabs  13988  rescabs2  13989  resssetc  14202  resscatc  14215  yonedalem1  14324  yonedalem21  14325  yonedalem3a  14326  yonedalem4c  14329  yonedalem22  14330  yonedalem3b  14331  yonedainv  14333  yonffthlem  14334  acsdomd  14562  gass  15033  sylow2blem2  15210  dprdres  15541  mplsubglem  16453  mpllsslem  16454  opsrtoslem2  16500  neiptoptop  17150  lpval  17158  neitr  17198  ordtbaslem  17206  ordtrest2  17222  cnrest2  17304  cnpresti  17306  cnprest  17307  cnprest2  17308  consuba  17436  consubclo  17440  uncon  17445  1stcelcls  17477  hausmapdom  17516  ptbasfi  17566  ptcls  17601  cnmpt2res  17662  qtopval2  17681  elqtop  17682  qtoprest  17702  ptuncnv  17792  ptunhmeo  17793  fsubbas  17852  elfm  17932  rnelfmlem  17937  rnelfm  17938  fmfnfmlem4  17942  flimclslem  17969  hauspwpwdom  17973  ptcmplem1  18036  cnextcn  18051  cnextfres  18052  isust  18186  ustssel  18188  trust  18212  elutop  18216  restutop  18220  trcfilu  18277  cfiluweak  18278  xmetres2  18344  fmcfil  19178  dvnf  19766  dvnbss  19767  dvaddf  19781  dvmulf  19782  dvcmulf  19784  dvcof  19787  ulmss  20266  wlks  21479  trls  21489  lmlim  24286  esummono  24403  esumpinfval  24416  cvmliftmolem1  24921  neibastop1  26278  neibastop2lem  26279  fnejoin1  26287  filnetlem3  26299  filnetlem4  26300  elrfi  26638  elrfirn2  26640  pwssplit0  27055  pwssplit1  27056  pwssplit2  27057  pwssplit3  27058  frlmsplit2  27111  frlmsslss  27112  pmtrfconj  27275  stoweidlem31  27647  stoweidlem53  27669  stoweidlem57  27673  stoweidlem59  27675  bnj1413  29110
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator