Theorem ssexd 4165

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

Syntax hints:   → wi 4   ∈ wcel 2160  Vcvv 2756   ⊆ wss 3148

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4143

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2758  df-in 3154  df-ss 3161

This theorem is referenced by:  iotaexab  5221  fex2  5410  riotaexg  5863  opabbrex  5948  funexw  6145  f1imaen2g  6827  pw2f1odclem  6870  fiss  7015  genipv  7548  suplocexprlemlub  7763  hashfacen  10863  ovshftex  10875  strslssd  12576  ressbas2d  12597  ressval3d  12601  ressabsg  12605  restid2  12770  ptex  12786  divsfval  12822  divsfvalg  12823  igsumvalx  12883  issubmnd  12933  ress0g  12934  issubg2m  13161  releqgg  13192  eqgex  13193  eqgfval  13194  isghm  13215  ringidss  13418  reldvdsrsrg  13479  dvdsrvald  13480  dvdsrex  13485  unitgrp  13503  unitabl  13504  unitlinv  13513  unitrinv  13514  dvrfvald  13520  rdivmuldivd  13531  invrpropdg  13536  rhmunitinv  13565  subrgugrp  13624  aprval  13641  aprap  13645  sralemg  13797  srascag  13801  sravscag  13802  sraipg  13803  sraex  13805  2basgeng  14103  cnrest2  14257  cnptopresti  14259  cnptoprest  14260  cnptoprest2  14261  cnmpt2res  14318  psmetres2  14354  xmetres2  14400  limccnp2lem  14683  limccnp2cntop  14684  dvfvalap  14688  dvmulxxbr  14704  dvaddxx  14705  dvmulxx  14706  dviaddf  14707  dvimulf  14708  dvcoapbr  14709  dvmptaddx  14719  dvmptmulx  14720