Theorem ssexd 4227

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

Syntax hints:   → wi 4   ∈ wcel 2200  Vcvv 2800   ⊆ wss 3198

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 4205

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 2802  df-in 3204  df-ss 3211

This theorem is referenced by:  iotaexab  5303  fex2  5500  riotaexg  5970  opabbrex  6060  funexw  6269  opabex2  6352  f1imaen2g  6962  pw2f1odclem  7015  fiss  7167  genipv  7719  suplocexprlemlub  7934  hashfacen  11090  ovshftex  11370  strslssd  13119  ressbas2d  13141  ressval3d  13145  ressabsg  13149  restid2  13321  ptex  13337  prdsval  13346  prdsbaslemss  13347  divsfval  13401  divsfvalg  13402  igsumvalx  13462  issubmnd  13515  ress0g  13516  issubg2m  13766  releqgg  13797  eqgex  13798  eqgfval  13799  isghm  13820  ringidss  14032  dvdsrvald  14097  dvdsrex  14102  unitgrp  14120  unitabl  14121  unitlinv  14130  unitrinv  14131  dvrfvald  14137  rdivmuldivd  14148  invrpropdg  14153  rhmunitinv  14182  subrgugrp  14244  aprval  14286  aprap  14290  sralemg  14442  srascag  14446  sravscag  14447  sraipg  14448  sraex  14450  2basgeng  14796  cnrest2  14950  cnptopresti  14952  cnptoprest  14953  cnptoprest2  14954  cnmpt2res  15011  psmetres2  15047  xmetres2  15093  limccnp2lem  15390  limccnp2cntop  15391  dvfvalap  15395  dvmulxxbr  15416  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  dvcoapbr  15421  dvmptaddx  15433  dvmptmulx  15434  plycj  15475  wksfval  16119  wlkex  16122  trlsfvalg  16178  trlsex  16182  eupthsg  16240