Theorem ssexd 4805

Description: A subclass of a set is a set. Deduction form of ssexg 4804. (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

Step	Hyp	Ref	Expression
1		ssexd.2	. 2 |- ( ph -> A C_ B )
2		ssexd.1	. 2 |- ( ph -> B e. C )
3		ssexg 4804	. 2 |- ( ( A C_ B /\ B e. C ) -> A e. _V )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 1990   _Vcvv 3200   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  sselpwd  4807  opabbrex  6695  soex  7109  fex2  7121  opabex2  7227  fnwelem  7292  fnse  7294  extmptsuppeq  7319  f1imaen2g  8017  ordtypelem10  8432  oismo  8445  wofib  8450  wemapso  8456  wdom2d  8485  wdomd  8486  unxpwdom2  8493  cantnfle  8568  cantnflt  8569  cantnflt2  8570  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cnfcom  8597  cnfcom2lem  8598  acni2  8869  fin1a2lem12  9233  hsmexlem1  9248  zorn2lem4  9321  fpwwe2lem2  9454  fpwwe2lem5  9456  fpwwe2lem12  9463  fpwwe2  9465  fpwwelem  9467  canthwelem  9472  pwfseqlem4  9484  trclfv  13741  hashbcss  15708  strssd  15909  restid2  16091  divsfval  16207  mrieqv2d  16299  mrissmrcd  16300  mreexexlemd  16304  mreexexlem3d  16306  mreexexlem4d  16307  mreexexdOLD  16309  mreexdomd  16310  rescabs  16493  rescabs2  16494  resssetc  16742  resscatc  16755  estrres  16779  yonedalem1  16912  yonedalem21  16913  yonedalem3a  16914  yonedalem4c  16917  yonedalem22  16918  yonedalem3b  16919  yonedainv  16921  yonffthlem  16922  joinfval  17001  meetfval  17015  acsdomd  17181  gass  17734  pmtrfconj  17886  sylow2blem2  18036  dprdres  18427  dmdprdsplitlem  18436  pwssplit0  19058  pwssplit1  19059  pwssplit2  19060  pwssplit3  19061  opsrtoslem2  19485  evls1gsumadd  19689  evls1gsummul  19690  evl1gsummul  19724  frlmsplit2  20112  frlmsslss  20113  neiptoptop  20935  lpval  20943  neitr  20984  ordtbaslem  20992  ordtrest2  21008  cnrest2  21090  cnpresti  21092  cnprest  21093  cnprest2  21094  connsuba  21223  connsubclo  21227  unconn  21232  1stcelcls  21264  hausmapdom  21303  dissnref  21331  ptbasfi  21384  ptcls  21419  cnmpt2res  21480  qtopval2  21499  elqtop  21500  qtoprest  21520  ptuncnv  21610  ptunhmeo  21611  fsubbas  21671  elfm  21751  rnelfmlem  21756  rnelfm  21757  fmfnfmlem4  21761  flimclslem  21788  hauspwpwdom  21792  ptcmplem1  21856  cnextcn  21871  cnextfres1  21872  isust  22007  trust  22033  elutop  22037  restutop  22041  trcfilu  22098  cfiluweak  22099  psmetres2  22119  xmetres2  22166  fmcfil  23070  dvnf  23690  dvnbss  23691  dvaddf  23705  dvmulf  23706  dvcmulf  23708  dvcof  23711  ulmss  24151  perpln1  25605  perpln2  25606  isperp  25607  wksfval  26505  resf1o  29505  ordtrest2NEW  29969  lmlim  29993  esummono  30116  esumrnmpt2  30130  esumpinfval  30135  carsgmon  30376  carsggect  30380  reprval  30688  repr0  30689  reprsuc  30693  reprss  30695  reprinrn  30696  reprlt  30697  reprgt  30699  reprinfz1  30700  reprpmtf1o  30704  reprdifc  30705  bnj1413  31103  cvmliftmolem1  31263  nosupno  31849  sssslt1  31906  sssslt2  31907  fwddifval  32269  neibastop1  32354  neibastop2lem  32355  fnejoin1  32363  filnetlem3  32375  filnetlem4  32376  dissneqlem  33187  elrfi  37257  elrfirn2  37259  clcnvlem  37930  relexpss1d  37997  k0004lem2  38446  ixpssmapc  39243  restuni4  39304  wessf1ornlem  39371  unirnmap  39400  inmap  39401  difmapsn  39404  unirnmapsn  39406  ssmapsn  39408  limsupre  39873  limsuppnfdlem  39933  limsuppnflem  39942  limsupmnflem  39952  limsupre2lem  39956  liminfval4  40021  liminfval3  40022  icccncfext  40100  dvdivcncf  40142  dvnprodlem1  40161  dvnprodlem2  40162  ovolsplit  40205  stoweidlem31  40248  stoweidlem53  40270  stoweidlem57  40274  stoweidlem59  40276  etransclem46  40497  saliuncl  40542  salexct  40552  subsaluni  40578  fsumlesge0  40594  sge0f1o  40599  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  meadjuni  40674  meadjiunlem  40682  omessle  40712  omecl  40717  isomenndlem  40744  caragencmpl  40749  ovnval2  40759  ovnval2b  40766  ovncvrrp  40778  ovncl  40781  hoidmvlelem2  40810  hoidmvlelem3  40811  ovncvr2  40825  ovnsubadd2lem  40859  ovnovollem3  40872  vonvolmbllem  40874  vonvolmbl  40875  sssmf  40947  incsmf  40951  issmflelem  40953  issmfle  40954  smfconst  40958  issmfgtlem  40964  issmfgt  40965  smfaddlem2  40972  decsmf  40975  issmfgelem  40977  issmfge  40978  nsssmfmbflem  40986  smfpimioo  40994  smfresal  40995  smfmullem4  41001  smfpimbor1lem1  41005  smf2id  41008  upwlksfval  41716