Theorem ssexd 4273

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  Vcvv 2821   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  sepab  4278  iotaexab  5356  fex2  5556  riotaexg  6042  opabbrex  6132  funexw  6341  opabex2  6428  f1imaen2g  7080  pw2f1odclem  7134  fiss  7311  genipv  7876  suplocexprlemlub  8091  hashfibclem  11282  hashfacen  11284  hashf1lem1  11285  ovshftex  11584  strslssd  13399  ressbas2d  13422  ressval3d  13426  ressabsg  13430  restid2  13602  ptex  13618  divsfval  13649  divsfvalg  13650  gzsumvalx  13709  issubmnd  13755  ress0g  13756  issubg2m  13992  releqgg  14023  eqgex  14024  eqgfval  14025  isghm  14046  prdsval  14173  prdsbaslemss  14174  ringidss  14334  dvdsrvald  14400  dvdsrex  14405  unitgrp  14423  unitabl  14424  unitlinv  14433  unitrinv  14434  dvrfvald  14440  rdivmuldivd  14451  invrpropdg  14456  rhmunitinv  14485  subrgugrp  14548  aprval  14591  aprap  14598  aprprop  14601  sralemg  14775  srascag  14779  sravscag  14780  sraipg  14781  sraex  14783  2basgeng  15183  cnrest2  15337  cnptopresti  15339  cnptoprest  15340  cnptoprest2  15341  cnmpt2res  15398  psmetres2  15434  xmetres2  15480  limccnp2lem  15777  limccnp2cntop  15778  dvfvalap  15782  dvmulxxbr  15803  dvaddxx  15804  dvmulxx  15805  dviaddf  15806  dvimulf  15807  dvcoapbr  15808  dvmptaddx  15820  dvmptmulx  15821  plycj  15862  wksfval  16563  wlkex  16566  trlsfvalg  16624  trlsex  16628  eupthsg  16686