Theorem ssexd 4028

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

Syntax hints:   -> wi 4   e. wcel 1463   _Vcvv 2657   C_ wss 3037

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-in 3043  df-ss 3050

This theorem is referenced by:  fex2  5249  riotaexg  5688  opabbrex  5769  f1imaen2g  6641  fiss  6817  genipv  7265  hashfacen  10472  ovshftex  10484  strslssd  11848  restid2  11972  2basgeng  12094  cnrest2  12247  cnptopresti  12249  cnptoprest  12250  cnptoprest2  12251  cnmpt2res  12308  psmetres2  12322  xmetres2  12368  limccnp2lem  12601  limccnp2cntop  12602  dvfvalap  12605  dvmulxxbr  12621  dvaddxx  12622  dvmulxx  12623  dviaddf  12624  dvimulf  12625