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  5494  riotaexg  5964  opabbrex  6054  funexw  6263  f1imaen2g  6953  pw2f1odclem  7003  fiss  7155  genipv  7707  suplocexprlemlub  7922  hashfacen  11071  ovshftex  11346  strslssd  13095  ressbas2d  13117  ressval3d  13121  ressabsg  13125  restid2  13297  ptex  13313  prdsval  13322  prdsbaslemss  13323  divsfval  13377  divsfvalg  13378  igsumvalx  13438  issubmnd  13491  ress0g  13492  issubg2m  13742  releqgg  13773  eqgex  13774  eqgfval  13775  isghm  13796  ringidss  14008  dvdsrvald  14073  dvdsrex  14078  unitgrp  14096  unitabl  14097  unitlinv  14106  unitrinv  14107  dvrfvald  14113  rdivmuldivd  14124  invrpropdg  14129  rhmunitinv  14158  subrgugrp  14220  aprval  14262  aprap  14266  sralemg  14418  srascag  14422  sravscag  14423  sraipg  14424  sraex  14426  2basgeng  14772  cnrest2  14926  cnptopresti  14928  cnptoprest  14929  cnptoprest2  14930  cnmpt2res  14987  psmetres2  15023  xmetres2  15069  limccnp2lem  15366  limccnp2cntop  15367  dvfvalap  15371  dvmulxxbr  15392  dvaddxx  15393  dvmulxx  15394  dviaddf  15395  dvimulf  15396  dvcoapbr  15397  dvmptaddx  15409  dvmptmulx  15410  plycj  15451  wksfval  16068  wlkex  16071  trlsfvalg  16127