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

Theorem ssexd 4442
Description: A subclass of a set is a set. Deduction form of ssexg 4441. (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 4441 . 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 1756   _Vcvv 2975    C_ wss 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338  df-ss 3345
This theorem is referenced by:  opabbrex  6133  opabex2  6519  soex  6524  fex2  6535  fnwelem  6690  fnse  6692  extmptsuppeq  6716  f1imaen2g  7373  ordtypelem10  7744  oismo  7757  wofib  7762  wemapso  7768  wdom2d  7798  wdomd  7799  unxpwdom2  7806  cantnfle  7882  cantnflt  7883  cantnflt2  7884  cantnfp1lem2  7890  cantnfp1lem3  7891  cantnflem1b  7897  cantnflem1d  7899  cantnflem1  7900  cantnfleOLD  7912  cantnfltOLD  7913  cantnflt2OLD  7914  cantnfp1lem2OLD  7916  cantnfp1lem3OLD  7917  cantnflem1bOLD  7920  cantnflem1dOLD  7922  cantnflem1OLD  7923  cnfcomlem  7935  cnfcom  7936  cnfcom2lem  7937  cnfcom3lem  7939  cnfcomlemOLD  7943  cnfcomOLD  7944  cnfcom2lemOLD  7945  cnfcom3lemOLD  7947  acni2  8219  fin1a2lem12  8583  hsmexlem1  8598  zorn2lem4  8671  fpwwe2lem2  8802  fpwwe2lem5  8804  fpwwe2lem12  8811  fpwwe2  8813  fpwwelem  8815  canthwelem  8820  pwfseqlem4  8832  hashbcss  14068  strssd  14213  restid2  14372  divsfval  14488  mrieqv2d  14580  mrissmrcd  14581  mreexexlemd  14585  mreexexlem3d  14587  mreexexlem4d  14588  mreexexd  14589  mreexdomd  14590  rescabs  14749  rescabs2  14750  resssetc  14963  resscatc  14976  yonedalem1  15085  yonedalem21  15086  yonedalem3a  15087  yonedalem4c  15090  yonedalem22  15091  yonedalem3b  15092  yonedainv  15094  yonffthlem  15095  joinfval  15174  meetfval  15188  acsdomd  15354  gass  15822  pmtrfconj  15975  sylow2blem2  16123  dprdres  16528  dmdprdsplitlem  16537  pwssplit0  17142  pwssplit1  17143  pwssplit2  17144  pwssplit3  17145  mplsubglemOLD  17515  mpllsslemOLD  17516  opsrtoslem2  17569  evls1gsumadd  17762  evls1gsummul  17763  evl1gsummul  17797  frlmsplit2  18200  frlmsslss  18201  neiptoptop  18738  lpval  18746  neitr  18787  ordtbaslem  18795  ordtrest2  18811  cnrest2  18893  cnpresti  18895  cnprest  18896  cnprest2  18897  consuba  19027  consubclo  19031  uncon  19036  1stcelcls  19068  hausmapdom  19107  ptbasfi  19157  ptcls  19192  cnmpt2res  19253  qtopval2  19272  elqtop  19273  qtoprest  19293  ptuncnv  19383  ptunhmeo  19384  fsubbas  19443  elfm  19523  rnelfmlem  19528  rnelfm  19529  fmfnfmlem4  19533  flimclslem  19560  hauspwpwdom  19564  ptcmplem1  19627  cnextcn  19642  cnextfres  19643  isust  19781  ustssel  19783  trust  19807  elutop  19811  restutop  19815  trcfilu  19872  cfiluweak  19873  xmetres2  19939  fmcfil  20786  dvnf  21404  dvnbss  21405  dvaddf  21419  dvmulf  21420  dvcmulf  21422  dvcof  21425  ulmss  21865  wlks  23428  trls  23438  ordtrest2NEW  26356  lmlim  26380  esummono  26512  esumpinfval  26525  cvmliftmolem1  27173  neibastop1  28583  neibastop2lem  28584  fnejoin1  28592  filnetlem3  28604  filnetlem4  28605  elrfi  29033  elrfirn2  29035  stoweidlem31  29829  stoweidlem53  29851  stoweidlem57  29855  stoweidlem59  29857  bnj1413  32029
  Copyright terms: Public domain W3C validator