Theorem ssexd 4144

Description: A subclass of a set is a set. Deduction form of ssexg 4143. (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 4143	. 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 2738   C_ wss 3130

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 4122

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 2740  df-in 3136  df-ss 3143

This theorem is referenced by:  fex2  5385  riotaexg  5835  opabbrex  5919  funexw  6113  f1imaen2g  6793  fiss  6976  genipv  7508  suplocexprlemlub  7723  hashfacen  10816  ovshftex  10828  strslssd  12509  ressbas2d  12528  ressval3d  12531  ressabsg  12535  restid2  12697  ptex  12713  divsfvalg  12748  issubmnd  12843  ress0g  12844  issubg2m  13049  releqgg  13080  eqgfval  13081  ringidss  13212  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrex  13267  unitgrp  13285  unitabl  13286  unitlinv  13295  unitrinv  13296  dvrfvald  13302  rdivmuldivd  13313  invrpropdg  13318  subrgugrp  13361  aprval  13372  aprap  13376  2basgeng  13585  cnrest2  13739  cnptopresti  13741  cnptoprest  13742  cnptoprest2  13743  cnmpt2res  13800  psmetres2  13836  xmetres2  13882  limccnp2lem  14148  limccnp2cntop  14149  dvfvalap  14153  dvmulxxbr  14169  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvcoapbr  14174  dvmptaddx  14184  dvmptmulx  14185