Theorem ssexd 4224

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

Syntax hints:   → wi 4   ∈ wcel 2200  Vcvv 2799   ⊆ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210

This theorem is referenced by:  iotaexab  5297  fex2  5492  riotaexg  5958  opabbrex  6048  funexw  6257  f1imaen2g  6945  pw2f1odclem  6995  fiss  7144  genipv  7696  suplocexprlemlub  7911  hashfacen  11058  ovshftex  11330  strslssd  13079  ressbas2d  13101  ressval3d  13105  ressabsg  13109  restid2  13281  ptex  13297  prdsval  13306  prdsbaslemss  13307  divsfval  13361  divsfvalg  13362  igsumvalx  13422  issubmnd  13475  ress0g  13476  issubg2m  13726  releqgg  13757  eqgex  13758  eqgfval  13759  isghm  13780  ringidss  13992  dvdsrvald  14057  dvdsrex  14062  unitgrp  14080  unitabl  14081  unitlinv  14090  unitrinv  14091  dvrfvald  14097  rdivmuldivd  14108  invrpropdg  14113  rhmunitinv  14142  subrgugrp  14204  aprval  14246  aprap  14250  sralemg  14402  srascag  14406  sravscag  14407  sraipg  14408  sraex  14410  2basgeng  14756  cnrest2  14910  cnptopresti  14912  cnptoprest  14913  cnptoprest2  14914  cnmpt2res  14971  psmetres2  15007  xmetres2  15053  limccnp2lem  15350  limccnp2cntop  15351  dvfvalap  15355  dvmulxxbr  15376  dvaddxx  15377  dvmulxx  15378  dviaddf  15379  dvimulf  15380  dvcoapbr  15381  dvmptaddx  15393  dvmptmulx  15394  plycj  15435  wksfval  16035