Theorem ssexd 4170

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

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 4148

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 3160  df-ss 3167

This theorem is referenced by:  iotaexab  5234  fex2  5423  riotaexg  5878  opabbrex  5963  funexw  6166  f1imaen2g  6849  pw2f1odclem  6892  fiss  7038  genipv  7571  suplocexprlemlub  7786  hashfacen  10910  ovshftex  10966  strslssd  12668  ressbas2d  12689  ressval3d  12693  ressabsg  12697  restid2  12862  ptex  12878  divsfval  12914  divsfvalg  12915  igsumvalx  12975  issubmnd  13026  ress0g  13027  issubg2m  13262  releqgg  13293  eqgex  13294  eqgfval  13295  isghm  13316  ringidss  13528  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrex  13597  unitgrp  13615  unitabl  13616  unitlinv  13625  unitrinv  13626  dvrfvald  13632  rdivmuldivd  13643  invrpropdg  13648  rhmunitinv  13677  subrgugrp  13739  aprval  13781  aprap  13785  sralemg  13937  srascag  13941  sravscag  13942  sraipg  13943  sraex  13945  2basgeng  14261  cnrest2  14415  cnptopresti  14417  cnptoprest  14418  cnptoprest2  14419  cnmpt2res  14476  psmetres2  14512  xmetres2  14558  limccnp2lem  14855  limccnp2cntop  14856  dvfvalap  14860  dvmulxxbr  14881  dvaddxx  14882  dvmulxx  14883  dviaddf  14884  dvimulf  14885  dvcoapbr  14886  dvmptaddx  14898  dvmptmulx  14899  plycj  14939