Theorem ssexd 4169

Description: A subclass of a set is a set. Deduction form of ssexg 4168. (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 4168	. 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 2164   _Vcvv 2760   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159  df-ss 3166

This theorem is referenced by:  iotaexab  5233  fex2  5422  riotaexg  5877  opabbrex  5962  funexw  6164  f1imaen2g  6847  pw2f1odclem  6890  fiss  7036  genipv  7569  suplocexprlemlub  7784  hashfacen  10907  ovshftex  10963  strslssd  12665  ressbas2d  12686  ressval3d  12690  ressabsg  12694  restid2  12859  ptex  12875  divsfval  12911  divsfvalg  12912  igsumvalx  12972  issubmnd  13023  ress0g  13024  issubg2m  13259  releqgg  13290  eqgex  13291  eqgfval  13292  isghm  13313  ringidss  13525  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrex  13594  unitgrp  13612  unitabl  13613  unitlinv  13622  unitrinv  13623  dvrfvald  13629  rdivmuldivd  13640  invrpropdg  13645  rhmunitinv  13674  subrgugrp  13736  aprval  13778  aprap  13782  sralemg  13934  srascag  13938  sravscag  13939  sraipg  13940  sraex  13942  2basgeng  14250  cnrest2  14404  cnptopresti  14406  cnptoprest  14407  cnptoprest2  14408  cnmpt2res  14465  psmetres2  14501  xmetres2  14547  limccnp2lem  14830  limccnp2cntop  14831  dvfvalap  14835  dvmulxxbr  14851  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvcoapbr  14856  dvmptaddx  14866  dvmptmulx  14867