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

Theorem ssexd 4584
Description: A subclass of a set is a set. Deduction form of ssexg 4583. (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 4583 . 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 1804   _Vcvv 3095    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475
This theorem is referenced by:  opabbrex  6324  opabbrexOLD  6325  opabex2  6723  soex  6728  fex2  6740  fnwelem  6900  fnse  6902  extmptsuppeq  6926  f1imaen2g  7578  ordtypelem10  7955  oismo  7968  wofib  7973  wemapso  7979  wdom2d  8009  wdomd  8010  unxpwdom2  8017  cantnfle  8093  cantnflt  8094  cantnflt2  8095  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1d  8110  cantnflem1  8111  cantnfleOLD  8123  cantnfltOLD  8124  cantnflt2OLD  8125  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  cnfcomlem  8146  cnfcom  8147  cnfcom2lem  8148  cnfcom3lem  8150  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom2lemOLD  8156  cnfcom3lemOLD  8158  acni2  8430  fin1a2lem12  8794  hsmexlem1  8809  zorn2lem4  8882  fpwwe2lem2  9013  fpwwe2lem5  9015  fpwwe2lem12  9022  fpwwe2  9024  fpwwelem  9026  canthwelem  9031  pwfseqlem4  9043  hashbcss  14399  strssd  14545  restid2  14705  divsfval  14821  mrieqv2d  14913  mrissmrcd  14914  mreexexlemd  14918  mreexexlem3d  14920  mreexexlem4d  14921  mreexexd  14922  mreexdomd  14923  rescabs  15079  rescabs2  15080  resssetc  15293  resscatc  15306  yonedalem1  15415  yonedalem21  15416  yonedalem3a  15417  yonedalem4c  15420  yonedalem22  15421  yonedalem3b  15422  yonedainv  15424  yonffthlem  15425  joinfval  15505  meetfval  15519  acsdomd  15685  gass  16213  pmtrfconj  16365  sylow2blem2  16515  dprdres  16949  dmdprdsplitlem  16958  pwssplit0  17578  pwssplit1  17579  pwssplit2  17580  pwssplit3  17581  mplsubglemOLD  17969  mpllsslemOLD  17970  opsrtoslem2  18023  evls1gsumadd  18235  evls1gsummul  18236  evl1gsummul  18270  frlmsplit2  18676  frlmsslss  18677  neiptoptop  19505  lpval  19513  neitr  19554  ordtbaslem  19562  ordtrest2  19578  cnrest2  19660  cnpresti  19662  cnprest  19663  cnprest2  19664  consuba  19794  consubclo  19798  uncon  19803  1stcelcls  19835  hausmapdom  19874  dissnref  19902  ptbasfi  19955  ptcls  19990  cnmpt2res  20051  qtopval2  20070  elqtop  20071  qtoprest  20091  ptuncnv  20181  ptunhmeo  20182  fsubbas  20241  elfm  20321  rnelfmlem  20326  rnelfm  20327  fmfnfmlem4  20331  flimclslem  20358  hauspwpwdom  20362  ptcmplem1  20425  cnextcn  20440  cnextfres  20441  isust  20579  ustssel  20581  trust  20605  elutop  20609  restutop  20613  trcfilu  20670  cfiluweak  20671  psmetres2  20691  xmetres2  20737  fmcfil  21584  dvnf  22203  dvnbss  22204  dvaddf  22218  dvmulf  22219  dvcmulf  22221  dvcof  22224  ulmss  22664  perpln1  23959  perpln2  23960  isperp  23961  wlks  24391  trls  24410  resf1o  27425  crefi  27723  ordtrest2NEW  27778  lmlim  27802  esummono  27939  esumpinfval  27952  omsfval  28138  cvmliftmolem1  28599  neibastop1  30152  neibastop2lem  30153  fnejoin1  30161  filnetlem3  30173  filnetlem4  30174  elrfi  30601  elrfirn2  30603  limsupre  31555  icccncfext  31597  dvdivcncf  31628  stoweidlem31  31702  stoweidlem53  31724  stoweidlem57  31728  stoweidlem59  31730  estrres  32494  bnj1413  33824
  Copyright terms: Public domain W3C validator