Theorem ssex 5290

Description: A subclass of a set is a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 5256 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) (Proof shortened by BJ, 18-Jul-2026.)

Hypothesis

Ref	Expression
ssex.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ssex	⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Proof of Theorem ssex

Step	Hyp	Ref	Expression
1		ssex.1	. 2 ⊢ 𝐵 ∈ V
2		ssexg 5289	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
3	1, 2	mpan2 703	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921

This theorem is used by:  ssexi  5292  ssexgOLD  5293  intex  5313  moabexOLD  5439  naddunif  8678  ixpiunwdom  9550  omex  9610  tcss  9709  bndrank  9811  scottex  9860  scottexOLD  9861  aceq3lem  10111  cfslb  10256  dcomex  10437  axdc2lem  10438  grothpw  10817  grothpwex  10818  grothomex  10820  elnp  10978  negfi  12170  limsuple  15536  limsuplt  15537  limsupbnd1  15540  o1add2  15682  o1mul2  15683  o1sub2  15684  o1dif  15688  caucvgrlem  15731  fsumo1  15871  lcmfval  16685  lcmf0val  16686  unbenlem  16974  ressbas2  17304  prdsval  17514  prdsbas  17516  rescbas  17892  reschom  17893  rescco  17895  acsmapd  18616  issstrmgm  18717  issubmgm2  18767  issubmnd  18825  eqgfval  19250  dfod2  19640  ablfac1b  20148  islinds2  21974  pmatcollpw3lem  22951  2basgen  23158  prdstopn  23796  ressust  24431  rectbntr0  25001  elcncf  25059  cncfcnvcn  25095  cmssmscld  25520  cmsss  25521  ovolctb2  25662  limcfval  26042  ellimc2  26047  limcflf  26051  limcres  26056  limcun  26065  dvfval  26067  lhop2  26185  taylfval  26533  ulmval  26554  xrlimcnp  27144  axtgcont1  28748  ressnm  33293  ressprs  33295  ordtrestNEW  34320  ddeval1  34633  ddeval0  34634  carsgclctunlem3  34719  bnj849  35322  msrval  36038  mclsval  36063  brsset  36387  isfne4  36879  refssfne  36897  topjoin  36904  bj-snglex  37637  mblfinlem3  38338  filbcmb  38419  cnpwstotbnd  38476  ismtyval  38479  ispsubsp  40547  ispsubclN  40739  isnumbasgrplem2  43859  rtrclex  44371  brmptiunrelexpd  44437  iunrelexp0  44456  mulcncff  46612  subcncff  46622  addcncff  46626  cncfuni  46628  divcncff  46633  etransclem1  46977  etransclem4  46980  etransclem13  46989  isvonmbl  47380  isubgriedg  48656  isubgrvtx  48660  uhgrimisgrgric  48724  linccl  49222  ellcoellss  49243  elbigolo1  49365