Theorem ssexd 4229

Description: A subclass of a set is a set. Deduction form of ssexg 4228. (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 4228	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2202  Vcvv 2802   ⊆ wss 3200

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206  df-ss 3213

This theorem is referenced by:  iotaexab  5305  fex2  5503  riotaexg  5974  opabbrex  6064  funexw  6273  opabex2  6356  f1imaen2g  6966  pw2f1odclem  7019  fiss  7175  genipv  7728  suplocexprlemlub  7943  hashfacen  11099  ovshftex  11379  strslssd  13128  ressbas2d  13150  ressval3d  13154  ressabsg  13158  restid2  13330  ptex  13346  prdsval  13355  prdsbaslemss  13356  divsfval  13410  divsfvalg  13411  igsumvalx  13471  issubmnd  13524  ress0g  13525  issubg2m  13775  releqgg  13806  eqgex  13807  eqgfval  13808  isghm  13829  ringidss  14041  dvdsrvald  14106  dvdsrex  14111  unitgrp  14129  unitabl  14130  unitlinv  14139  unitrinv  14140  dvrfvald  14146  rdivmuldivd  14157  invrpropdg  14162  rhmunitinv  14191  subrgugrp  14253  aprval  14295  aprap  14299  sralemg  14451  srascag  14455  sravscag  14456  sraipg  14457  sraex  14459  2basgeng  14805  cnrest2  14959  cnptopresti  14961  cnptoprest  14962  cnptoprest2  14963  cnmpt2res  15020  psmetres2  15056  xmetres2  15102  limccnp2lem  15399  limccnp2cntop  15400  dvfvalap  15404  dvmulxxbr  15425  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  dvcoapbr  15430  dvmptaddx  15442  dvmptmulx  15443  plycj  15484  wksfval  16172  wlkex  16175  trlsfvalg  16233  trlsex  16237  eupthsg  16295