Theorem ssexd 4173

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

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  5237  fex2  5426  riotaexg  5881  opabbrex  5966  funexw  6169  f1imaen2g  6852  pw2f1odclem  6895  fiss  7043  genipv  7576  suplocexprlemlub  7791  hashfacen  10928  ovshftex  10984  strslssd  12725  ressbas2d  12746  ressval3d  12750  ressabsg  12754  restid2  12919  ptex  12935  divsfval  12971  divsfvalg  12972  igsumvalx  13032  issubmnd  13083  ress0g  13084  issubg2m  13319  releqgg  13350  eqgex  13351  eqgfval  13352  isghm  13373  ringidss  13585  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrex  13654  unitgrp  13672  unitabl  13673  unitlinv  13682  unitrinv  13683  dvrfvald  13689  rdivmuldivd  13700  invrpropdg  13705  rhmunitinv  13734  subrgugrp  13796  aprval  13838  aprap  13842  sralemg  13994  srascag  13998  sravscag  13999  sraipg  14000  sraex  14002  2basgeng  14318  cnrest2  14472  cnptopresti  14474  cnptoprest  14475  cnptoprest2  14476  cnmpt2res  14533  psmetres2  14569  xmetres2  14615  limccnp2lem  14912  limccnp2cntop  14913  dvfvalap  14917  dvmulxxbr  14938  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  dvcoapbr  14943  dvmptaddx  14955  dvmptmulx  14956  plycj  14997