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

Theorem ssexd 4436
Description: A subclass of a set is a set. Deduction form of ssexg 4435. (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 4435 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 656 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   _Vcvv 2970    C_ wss 3325
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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-ss 3339
This theorem is referenced by:  opabbrex  6129  opabex2  6515  soex  6520  fex2  6531  fnwelem  6686  fnse  6688  extmptsuppeq  6712  f1imaen2g  7366  ordtypelem10  7737  oismo  7750  wofib  7755  wemapso  7761  wdom2d  7791  wdomd  7792  unxpwdom2  7799  cantnfle  7875  cantnflt  7876  cantnflt2  7877  cantnfp1lem2  7883  cantnfp1lem3  7884  cantnflem1b  7890  cantnflem1d  7892  cantnflem1  7893  cantnfleOLD  7905  cantnfltOLD  7906  cantnflt2OLD  7907  cantnfp1lem2OLD  7909  cantnfp1lem3OLD  7910  cantnflem1bOLD  7913  cantnflem1dOLD  7915  cantnflem1OLD  7916  cnfcomlem  7928  cnfcom  7929  cnfcom2lem  7930  cnfcom3lem  7932  cnfcomlemOLD  7936  cnfcomOLD  7937  cnfcom2lemOLD  7938  cnfcom3lemOLD  7940  acni2  8212  fin1a2lem12  8576  hsmexlem1  8591  zorn2lem4  8664  fpwwe2lem2  8795  fpwwe2lem5  8797  fpwwe2lem12  8804  fpwwe2  8806  fpwwelem  8808  canthwelem  8813  pwfseqlem4  8825  hashbcss  14061  strssd  14206  restid2  14365  divsfval  14481  mrieqv2d  14573  mrissmrcd  14574  mreexexlemd  14578  mreexexlem3d  14580  mreexexlem4d  14581  mreexexd  14582  mreexdomd  14583  rescabs  14742  rescabs2  14743  resssetc  14956  resscatc  14969  yonedalem1  15078  yonedalem21  15079  yonedalem3a  15080  yonedalem4c  15083  yonedalem22  15084  yonedalem3b  15085  yonedainv  15087  yonffthlem  15088  joinfval  15167  meetfval  15181  acsdomd  15347  gass  15812  pmtrfconj  15965  sylow2blem2  16113  dprdres  16515  dmdprdsplitlem  16524  pwssplit0  17117  pwssplit1  17118  pwssplit2  17119  pwssplit3  17120  mplsubglemOLD  17490  mpllsslemOLD  17491  opsrtoslem2  17542  frlmsplit2  18156  frlmsslss  18157  neiptoptop  18694  lpval  18702  neitr  18743  ordtbaslem  18751  ordtrest2  18767  cnrest2  18849  cnpresti  18851  cnprest  18852  cnprest2  18853  consuba  18983  consubclo  18987  uncon  18992  1stcelcls  19024  hausmapdom  19063  ptbasfi  19113  ptcls  19148  cnmpt2res  19209  qtopval2  19228  elqtop  19229  qtoprest  19249  ptuncnv  19339  ptunhmeo  19340  fsubbas  19399  elfm  19479  rnelfmlem  19484  rnelfm  19485  fmfnfmlem4  19489  flimclslem  19516  hauspwpwdom  19520  ptcmplem1  19583  cnextcn  19598  cnextfres  19599  isust  19737  ustssel  19739  trust  19763  elutop  19767  restutop  19771  trcfilu  19828  cfiluweak  19829  xmetres2  19895  fmcfil  20742  dvnf  21360  dvnbss  21361  dvaddf  21375  dvmulf  21376  dvcmulf  21378  dvcof  21381  ulmss  21821  wlks  23360  trls  23370  ordtrest2NEW  26289  lmlim  26313  esummono  26445  esumpinfval  26458  cvmliftmolem1  27100  neibastop1  28505  neibastop2lem  28506  fnejoin1  28514  filnetlem3  28526  filnetlem4  28527  elrfi  28955  elrfirn2  28957  stoweidlem31  29751  stoweidlem53  29773  stoweidlem57  29777  stoweidlem59  29779  bnj1413  31860
  Copyright terms: Public domain W3C validator