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

Theorem ssexd 4587
Description: A subclass of a set is a set. Deduction form of ssexg 4586. (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 4586 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   _Vcvv 3106    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483
This theorem is referenced by:  opabbrex  6315  opabex2  6712  soex  6717  fex2  6729  fnwelem  6888  fnse  6890  extmptsuppeq  6914  f1imaen2g  7566  ordtypelem10  7941  oismo  7954  wofib  7959  wemapso  7965  wdom2d  7995  wdomd  7996  unxpwdom2  8003  cantnfle  8079  cantnflt  8080  cantnflt2  8081  cantnfp1lem2  8087  cantnfp1lem3  8088  cantnflem1b  8094  cantnflem1d  8096  cantnflem1  8097  cantnfleOLD  8109  cantnfltOLD  8110  cantnflt2OLD  8111  cantnfp1lem2OLD  8113  cantnfp1lem3OLD  8114  cantnflem1bOLD  8117  cantnflem1dOLD  8119  cantnflem1OLD  8120  cnfcomlem  8132  cnfcom  8133  cnfcom2lem  8134  cnfcom3lem  8136  cnfcomlemOLD  8140  cnfcomOLD  8141  cnfcom2lemOLD  8142  cnfcom3lemOLD  8144  acni2  8416  fin1a2lem12  8780  hsmexlem1  8795  zorn2lem4  8868  fpwwe2lem2  8999  fpwwe2lem5  9001  fpwwe2lem12  9008  fpwwe2  9010  fpwwelem  9012  canthwelem  9017  pwfseqlem4  9029  hashbcss  14370  strssd  14515  restid2  14675  divsfval  14791  mrieqv2d  14883  mrissmrcd  14884  mreexexlemd  14888  mreexexlem3d  14890  mreexexlem4d  14891  mreexexd  14892  mreexdomd  14893  rescabs  15052  rescabs2  15053  resssetc  15266  resscatc  15279  yonedalem1  15388  yonedalem21  15389  yonedalem3a  15390  yonedalem4c  15393  yonedalem22  15394  yonedalem3b  15395  yonedainv  15397  yonffthlem  15398  joinfval  15477  meetfval  15491  acsdomd  15657  gass  16127  pmtrfconj  16280  sylow2blem2  16430  dprdres  16858  dmdprdsplitlem  16867  pwssplit0  17480  pwssplit1  17481  pwssplit2  17482  pwssplit3  17483  mplsubglemOLD  17859  mpllsslemOLD  17860  opsrtoslem2  17913  evls1gsumadd  18125  evls1gsummul  18126  evl1gsummul  18160  frlmsplit2  18563  frlmsslss  18564  neiptoptop  19391  lpval  19399  neitr  19440  ordtbaslem  19448  ordtrest2  19464  cnrest2  19546  cnpresti  19548  cnprest  19549  cnprest2  19550  consuba  19680  consubclo  19684  uncon  19689  1stcelcls  19721  hausmapdom  19760  ptbasfi  19810  ptcls  19845  cnmpt2res  19906  qtopval2  19925  elqtop  19926  qtoprest  19946  ptuncnv  20036  ptunhmeo  20037  fsubbas  20096  elfm  20176  rnelfmlem  20181  rnelfm  20182  fmfnfmlem4  20186  flimclslem  20213  hauspwpwdom  20217  ptcmplem1  20280  cnextcn  20295  cnextfres  20296  isust  20434  ustssel  20436  trust  20460  elutop  20464  restutop  20468  trcfilu  20525  cfiluweak  20526  xmetres2  20592  fmcfil  21439  dvnf  22058  dvnbss  22059  dvaddf  22073  dvmulf  22074  dvcmulf  22076  dvcof  22079  ulmss  22519  wlks  24181  trls  24200  ordtrest2NEW  27527  lmlim  27551  esummono  27692  esumpinfval  27705  cvmliftmolem1  28352  neibastop1  29767  neibastop2lem  29768  fnejoin1  29776  filnetlem3  29788  filnetlem4  29789  elrfi  30217  elrfirn2  30219  icccncfext  31181  dvdivcncf  31212  stoweidlem31  31286  stoweidlem53  31308  stoweidlem57  31312  stoweidlem59  31314  bnj1413  33045
  Copyright terms: Public domain W3C validator