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  5975  opabbrex  6065  funexw  6274  opabex2  6357  f1imaen2g  6967  pw2f1odclem  7020  fiss  7176  genipv  7729  suplocexprlemlub  7944  hashfacen  11101  ovshftex  11397  strslssd  13147  ressbas2d  13169  ressval3d  13173  ressabsg  13177  restid2  13349  ptex  13365  prdsval  13374  prdsbaslemss  13375  divsfval  13429  divsfvalg  13430  igsumvalx  13490  issubmnd  13543  ress0g  13544  issubg2m  13794  releqgg  13825  eqgex  13826  eqgfval  13827  isghm  13848  ringidss  14061  dvdsrvald  14126  dvdsrex  14131  unitgrp  14149  unitabl  14150  unitlinv  14159  unitrinv  14160  dvrfvald  14166  rdivmuldivd  14177  invrpropdg  14182  rhmunitinv  14211  subrgugrp  14273  aprval  14315  aprap  14319  sralemg  14471  srascag  14475  sravscag  14476  sraipg  14477  sraex  14479  2basgeng  14825  cnrest2  14979  cnptopresti  14981  cnptoprest  14982  cnptoprest2  14983  cnmpt2res  15040  psmetres2  15076  xmetres2  15122  limccnp2lem  15419  limccnp2cntop  15420  dvfvalap  15424  dvmulxxbr  15445  dvaddxx  15446  dvmulxx  15447  dviaddf  15448  dvimulf  15449  dvcoapbr  15450  dvmptaddx  15462  dvmptmulx  15463  plycj  15504  wksfval  16192  wlkex  16195  trlsfvalg  16253  trlsex  16257  eupthsg  16315