Theorem ssexd 4143

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

Syntax hints:   -> wi 4   e. wcel 2148   _Vcvv 2737   C_ wss 3129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-in 3135  df-ss 3142

This theorem is referenced by:  fex2  5384  riotaexg  5834  opabbrex  5918  funexw  6112  f1imaen2g  6792  fiss  6975  genipv  7507  suplocexprlemlub  7722  hashfacen  10815  ovshftex  10827  strslssd  12508  ressbas2d  12527  ressval3d  12530  ressabsg  12534  restid2  12696  ptex  12712  divsfvalg  12747  issubmnd  12842  ress0g  12843  issubg2m  13047  releqgg  13078  eqgfval  13079  ringidss  13210  reldvdsrsrg  13259  dvdsrvald  13260  dvdsrex  13265  unitgrp  13283  unitabl  13284  unitlinv  13293  unitrinv  13294  dvrfvald  13300  rdivmuldivd  13311  invrpropdg  13316  subrgugrp  13359  aprval  13370  aprap  13374  2basgeng  13552  cnrest2  13706  cnptopresti  13708  cnptoprest  13709  cnptoprest2  13710  cnmpt2res  13767  psmetres2  13803  xmetres2  13849  limccnp2lem  14115  limccnp2cntop  14116  dvfvalap  14120  dvmulxxbr  14136  dvaddxx  14137  dvmulxx  14138  dviaddf  14139  dvimulf  14140  dvcoapbr  14141  dvmptaddx  14151  dvmptmulx  14152