Theorem ssexd 4250

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

Syntax hints:   → wi 4   ∈ wcel 2203  Vcvv 2813   ⊆ wss 3211

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224

This theorem is referenced by:  iotaexab  5331  fex2  5531  riotaexg  6007  opabbrex  6097  funexw  6305  opabex2  6388  f1imaen2g  7033  pw2f1odclem  7087  fiss  7264  genipv  7824  suplocexprlemlub  8039  hashfibclem  11206  hashfacen  11208  ovshftex  11504  strslssd  13259  ressbas2d  13281  ressval3d  13285  ressabsg  13289  restid2  13461  ptex  13477  prdsval  13486  prdsbaslemss  13487  divsfval  13541  divsfvalg  13542  igsumvalx  13602  issubmnd  13655  ress0g  13656  issubg2m  13906  releqgg  13937  eqgex  13938  eqgfval  13939  isghm  13960  ringidss  14173  dvdsrvald  14238  dvdsrex  14243  unitgrp  14261  unitabl  14262  unitlinv  14271  unitrinv  14272  dvrfvald  14278  rdivmuldivd  14289  invrpropdg  14294  rhmunitinv  14323  subrgugrp  14385  aprval  14428  aprap  14432  sralemg  14586  srascag  14590  sravscag  14591  sraipg  14592  sraex  14594  2basgeng  14947  cnrest2  15101  cnptopresti  15103  cnptoprest  15104  cnptoprest2  15105  cnmpt2res  15162  psmetres2  15198  xmetres2  15244  limccnp2lem  15541  limccnp2cntop  15542  dvfvalap  15546  dvmulxxbr  15567  dvaddxx  15568  dvmulxx  15569  dviaddf  15570  dvimulf  15571  dvcoapbr  15572  dvmptaddx  15584  dvmptmulx  15585  plycj  15626  wksfval  16317  wlkex  16320  trlsfvalg  16378  trlsex  16382  eupthsg  16440