Theorem ssexd 4142

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

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  5383  riotaexg  5832  opabbrex  5916  funexw  6110  f1imaen2g  6790  fiss  6973  genipv  7505  suplocexprlemlub  7720  hashfacen  10809  ovshftex  10821  strslssd  12501  ressbas2d  12520  ressval3d  12523  ressabsg  12527  restid2  12685  issubmnd  12775  ress0g  12776  issubg2m  12980  releqgg  13011  eqgfval  13012  ringidss  13143  reldvdsrsrg  13192  dvdsrvald  13193  dvdsrex  13198  unitgrp  13216  unitabl  13217  unitlinv  13226  unitrinv  13227  dvrfvald  13233  rdivmuldivd  13244  invrpropdg  13249  aprval  13271  aprap  13275  subrgugrp  13299  2basgeng  13453  cnrest2  13607  cnptopresti  13609  cnptoprest  13610  cnptoprest2  13611  cnmpt2res  13668  psmetres2  13704  xmetres2  13750  limccnp2lem  14016  limccnp2cntop  14017  dvfvalap  14021  dvmulxxbr  14037  dvaddxx  14038  dvmulxx  14039  dviaddf  14040  dvimulf  14041  dvcoapbr  14042  dvmptaddx  14052  dvmptmulx  14053