Theorem ssexd 4174

Description: A subclass of a set is a set. Deduction form of ssexg 4173. (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 4173	. 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 2167   _Vcvv 2763   C_ wss 3157

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  iotaexab  5238  fex2  5429  riotaexg  5884  opabbrex  5970  funexw  6178  f1imaen2g  6861  pw2f1odclem  6904  fiss  7052  genipv  7593  suplocexprlemlub  7808  hashfacen  10945  ovshftex  11001  strslssd  12750  ressbas2d  12771  ressval3d  12775  ressabsg  12779  restid2  12950  ptex  12966  prdsval  12975  prdsbaslemss  12976  divsfval  13030  divsfvalg  13031  igsumvalx  13091  issubmnd  13144  ress0g  13145  issubg2m  13395  releqgg  13426  eqgex  13427  eqgfval  13428  isghm  13449  ringidss  13661  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrex  13730  unitgrp  13748  unitabl  13749  unitlinv  13758  unitrinv  13759  dvrfvald  13765  rdivmuldivd  13776  invrpropdg  13781  rhmunitinv  13810  subrgugrp  13872  aprval  13914  aprap  13918  sralemg  14070  srascag  14074  sravscag  14075  sraipg  14076  sraex  14078  2basgeng  14402  cnrest2  14556  cnptopresti  14558  cnptoprest  14559  cnptoprest2  14560  cnmpt2res  14617  psmetres2  14653  xmetres2  14699  limccnp2lem  14996  limccnp2cntop  14997  dvfvalap  15001  dvmulxxbr  15022  dvaddxx  15023  dvmulxx  15024  dviaddf  15025  dvimulf  15026  dvcoapbr  15027  dvmptaddx  15039  dvmptmulx  15040  plycj  15081