Theorem ssexd 4174

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

Syntax hints:   → wi 4   ∈ wcel 2167  Vcvv 2763   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  iotaexab  5238  fex2  5429  riotaexg  5884  opabbrex  5970  funexw  6178  f1imaen2g  6861  pw2f1odclem  6904  fiss  7052  genipv  7595  suplocexprlemlub  7810  hashfacen  10947  ovshftex  11003  strslssd  12752  ressbas2d  12773  ressval3d  12777  ressabsg  12781  restid2  12952  ptex  12968  prdsval  12977  prdsbaslemss  12978  divsfval  13032  divsfvalg  13033  igsumvalx  13093  issubmnd  13146  ress0g  13147  issubg2m  13397  releqgg  13428  eqgex  13429  eqgfval  13430  isghm  13451  ringidss  13663  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrex  13732  unitgrp  13750  unitabl  13751  unitlinv  13760  unitrinv  13761  dvrfvald  13767  rdivmuldivd  13778  invrpropdg  13783  rhmunitinv  13812  subrgugrp  13874  aprval  13916  aprap  13920  sralemg  14072  srascag  14076  sravscag  14077  sraipg  14078  sraex  14080  2basgeng  14426  cnrest2  14580  cnptopresti  14582  cnptoprest  14583  cnptoprest2  14584  cnmpt2res  14641  psmetres2  14677  xmetres2  14723  limccnp2lem  15020  limccnp2cntop  15021  dvfvalap  15025  dvmulxxbr  15046  dvaddxx  15047  dvmulxx  15048  dviaddf  15049  dvimulf  15050  dvcoapbr  15051  dvmptaddx  15063  dvmptmulx  15064  plycj  15105