Theorem ssex 5282

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 5249 (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 5281	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  ssexi  5284  ssexgOLD  5285  intex  5305  moabexOLD  5427  naddunif  8682  ixpiunwdom  9562  omex  9622  tcss  9721  bndrank  9824  scottex  9890  scottexOLD  9891  aceq3lem  10156  cfslb  10301  dcomex  10482  axdc2lem  10483  grothpw  10868  grothpwex  10869  grothomex  10871  elnp  11029  negfi  12221  limsuple  15598  limsuplt  15599  limsupbnd1  15602  o1add2  15744  o1mul2  15745  o1sub2  15746  o1dif  15750  caucvgrlem  15793  fsumo1  15932  lcmfval  16744  lcmf0val  16745  unbenlem  17033  ressbas2  17363  prdsval  17573  prdsbas  17575  rescbas  17951  reschom  17952  rescco  17954  acsmapd  18675  issstrmgm  18778  issubmgm2  18839  issubmnd  18900  eqgfval  19335  dfod2  19725  ablfac1b  20233  islinds2  22066  pmatcollpw3lem  23048  2basgen  23255  prdstopn  23894  ressust  24529  rectbntr0  25099  elcncf  25157  cncfcnvcn  25193  cmssmscld  25618  cmsss  25619  ovolctb2  25760  limcfval  26139  ellimc2  26144  limcflf  26148  limcres  26153  limcun  26162  dvfval  26164  lhop2  26282  taylfval  26635  ulmval  26656  xrlimcnp  27245  axtgcont1  28849  ressnm  33444  ressprs  33446  ordtrestNEW  34472  ddeval1  34786  ddeval0  34787  carsgclctunlem3  34872  bnj849  35475  msrval  36218  mclsval  36243  brsset  36567  isfne4  37044  refssfne  37062  topjoin  37069  bj-snglex  37802  mblfinlem3  38491  filbcmb  38588  cnpwstotbnd  38645  ismtyval  38648  ispsubsp  40716  ispsubclN  40908  isnumbasgrplem2  44043  rtrclex  44555  brmptiunrelexpd  44621  iunrelexp0  44640  mulcncff  46796  subcncff  46806  addcncff  46810  cncfuni  46812  divcncff  46817  etransclem1  47161  etransclem4  47164  etransclem13  47173  isvonmbl  47564  isubgriedg  48877  isubgrvtx  48881  uhgrimisgrgric  48945  linccl  49442  ellcoellss  49463  elbigolo1  49585