Theorem ssexd 4129

Description: A subclass of a set is a set. Deduction form of ssexg 4128. (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 4128	. 2 |- ( ( A C_ B /\ B e. C ) -> A e. _V )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 2141   _Vcvv 2730   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  fex2  5366  riotaexg  5813  opabbrex  5897  funexw  6091  f1imaen2g  6771  fiss  6954  genipv  7471  suplocexprlemlub  7686  hashfacen  10771  ovshftex  10783  strslssd  12462  restid2  12588  2basgeng  12876  cnrest2  13030  cnptopresti  13032  cnptoprest  13033  cnptoprest2  13034  cnmpt2res  13091  psmetres2  13127  xmetres2  13173  limccnp2lem  13439  limccnp2cntop  13440  dvfvalap  13444  dvmulxxbr  13460  dvaddxx  13461  dvmulxx  13462  dviaddf  13463  dvimulf  13464  dvcoapbr  13465  dvmptaddx  13475  dvmptmulx  13476