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

Theorem ssexd 4352
Description: A subclass of a set is a set. Deduction form of ssexg 4351. (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 4351 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   _Vcvv 2958    C_ wss 3322
This theorem is referenced by:  soex  5321  fex2  5605  opabbrex  6120  fnwelem  6463  fnse  6465  f1imaen2g  7170  ordtypelem10  7498  oismo  7511  wofib  7516  wemapso  7522  wdom2d  7550  wdomd  7551  unxpwdom2  7558  cantnfle  7628  cantnflt  7629  cantnflt2  7630  cantnfp1lem2  7637  cantnfp1lem3  7638  cantnflem1b  7644  cantnflem1d  7646  cantnflem1  7647  cnfcomlem  7658  cnfcom  7659  cnfcom2lem  7660  cnfcom3lem  7662  acni2  7929  fin1a2lem12  8293  hsmexlem1  8308  zorn2lem4  8381  fpwwe2lem2  8509  fpwwe2lem5  8511  fpwwe2lem12  8518  fpwwe2  8520  fpwwelem  8522  canthwelem  8527  pwfseqlem4  8539  hashbcss  13374  strssd  13505  restid2  13660  divsfval  13774  mrieqv2d  13866  mrissmrcd  13867  mreexexlemd  13871  mreexexlem3d  13873  mreexexlem4d  13874  mreexexd  13875  mreexdomd  13876  rescabs  14035  rescabs2  14036  resssetc  14249  resscatc  14262  yonedalem1  14371  yonedalem21  14372  yonedalem3a  14373  yonedalem4c  14376  yonedalem22  14377  yonedalem3b  14378  yonedainv  14380  yonffthlem  14381  acsdomd  14609  gass  15080  sylow2blem2  15257  dprdres  15588  mplsubglem  16500  mpllsslem  16501  opsrtoslem2  16547  neiptoptop  17197  lpval  17205  neitr  17246  ordtbaslem  17254  ordtrest2  17270  cnrest2  17352  cnpresti  17354  cnprest  17355  cnprest2  17356  consuba  17485  consubclo  17489  uncon  17494  1stcelcls  17526  hausmapdom  17565  ptbasfi  17615  ptcls  17650  cnmpt2res  17711  qtopval2  17730  elqtop  17731  qtoprest  17751  ptuncnv  17841  ptunhmeo  17842  fsubbas  17901  elfm  17981  rnelfmlem  17986  rnelfm  17987  fmfnfmlem4  17991  flimclslem  18018  hauspwpwdom  18022  ptcmplem1  18085  cnextcn  18100  cnextfres  18101  isust  18235  ustssel  18237  trust  18261  elutop  18265  restutop  18269  trcfilu  18326  cfiluweak  18327  xmetres2  18393  fmcfil  19227  dvnf  19815  dvnbss  19816  dvaddf  19830  dvmulf  19831  dvcmulf  19833  dvcof  19836  ulmss  20315  wlks  21528  trls  21538  lmlim  24335  esummono  24452  esumpinfval  24465  cvmliftmolem1  24970  neibastop1  26390  neibastop2lem  26391  fnejoin1  26399  filnetlem3  26411  filnetlem4  26412  elrfi  26750  elrfirn2  26752  pwssplit0  27166  pwssplit1  27167  pwssplit2  27168  pwssplit3  27169  frlmsplit2  27222  frlmsslss  27223  pmtrfconj  27386  stoweidlem31  27758  stoweidlem53  27780  stoweidlem57  27784  stoweidlem59  27786  bnj1413  29466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator