Theorem ssexd 4138

Description: A subclass of a set is a set. Deduction form of ssexg 4137. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
ssexd.1	⊢ (𝜑 → 𝐵 ∈ 𝐶)
ssexd.2	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssexd	⊢ (𝜑 → 𝐴 ∈ V)

Proof of Theorem ssexd

Step	Hyp	Ref	Expression
1		ssexd.2	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssexd.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
3		ssexg 4137	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2146  Vcvv 2735   ⊆ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-in 3133  df-ss 3140

This theorem is referenced by:  fex2  5376  riotaexg  5825  opabbrex  5909  funexw  6103  f1imaen2g  6783  fiss  6966  genipv  7483  suplocexprlemlub  7698  hashfacen  10784  ovshftex  10796  strslssd  12475  ressbas2d  12494  ressval3d  12497  ressabsg  12501  restid2  12628  2basgeng  13162  cnrest2  13316  cnptopresti  13318  cnptoprest  13319  cnptoprest2  13320  cnmpt2res  13377  psmetres2  13413  xmetres2  13459  limccnp2lem  13725  limccnp2cntop  13726  dvfvalap  13730  dvmulxxbr  13746  dvaddxx  13747  dvmulxx  13748  dviaddf  13749  dvimulf  13750  dvcoapbr  13751  dvmptaddx  13761  dvmptmulx  13762