Theorem ssexd 4200

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

Syntax hints:   → wi 4   ∈ wcel 2178  Vcvv 2776   ⊆ wss 3174

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-in 3180  df-ss 3187

This theorem is referenced by:  iotaexab  5269  fex2  5464  riotaexg  5926  opabbrex  6012  funexw  6220  f1imaen2g  6908  pw2f1odclem  6956  fiss  7105  genipv  7657  suplocexprlemlub  7872  hashfacen  11018  ovshftex  11245  strslssd  12994  ressbas2d  13015  ressval3d  13019  ressabsg  13023  restid2  13195  ptex  13211  prdsval  13220  prdsbaslemss  13221  divsfval  13275  divsfvalg  13276  igsumvalx  13336  issubmnd  13389  ress0g  13390  issubg2m  13640  releqgg  13671  eqgex  13672  eqgfval  13673  isghm  13694  ringidss  13906  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrex  13975  unitgrp  13993  unitabl  13994  unitlinv  14003  unitrinv  14004  dvrfvald  14010  rdivmuldivd  14021  invrpropdg  14026  rhmunitinv  14055  subrgugrp  14117  aprval  14159  aprap  14163  sralemg  14315  srascag  14319  sravscag  14320  sraipg  14321  sraex  14323  2basgeng  14669  cnrest2  14823  cnptopresti  14825  cnptoprest  14826  cnptoprest2  14827  cnmpt2res  14884  psmetres2  14920  xmetres2  14966  limccnp2lem  15263  limccnp2cntop  15264  dvfvalap  15268  dvmulxxbr  15289  dvaddxx  15290  dvmulxx  15291  dviaddf  15292  dvimulf  15293  dvcoapbr  15294  dvmptaddx  15306  dvmptmulx  15307  plycj  15348