Theorem ssexd 4185

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

Syntax hints:   → wi 4   ∈ wcel 2176  Vcvv 2772   ⊆ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  iotaexab  5251  fex2  5446  riotaexg  5905  opabbrex  5991  funexw  6199  f1imaen2g  6887  pw2f1odclem  6933  fiss  7081  genipv  7624  suplocexprlemlub  7839  hashfacen  10983  ovshftex  11163  strslssd  12912  ressbas2d  12933  ressval3d  12937  ressabsg  12941  restid2  13113  ptex  13129  prdsval  13138  prdsbaslemss  13139  divsfval  13193  divsfvalg  13194  igsumvalx  13254  issubmnd  13307  ress0g  13308  issubg2m  13558  releqgg  13589  eqgex  13590  eqgfval  13591  isghm  13612  ringidss  13824  reldvdsrsrg  13887  dvdsrvald  13888  dvdsrex  13893  unitgrp  13911  unitabl  13912  unitlinv  13921  unitrinv  13922  dvrfvald  13928  rdivmuldivd  13939  invrpropdg  13944  rhmunitinv  13973  subrgugrp  14035  aprval  14077  aprap  14081  sralemg  14233  srascag  14237  sravscag  14238  sraipg  14239  sraex  14241  2basgeng  14587  cnrest2  14741  cnptopresti  14743  cnptoprest  14744  cnptoprest2  14745  cnmpt2res  14802  psmetres2  14838  xmetres2  14884  limccnp2lem  15181  limccnp2cntop  15182  dvfvalap  15186  dvmulxxbr  15207  dvaddxx  15208  dvmulxx  15209  dviaddf  15210  dvimulf  15211  dvcoapbr  15212  dvmptaddx  15224  dvmptmulx  15225  plycj  15266