Theorem ssex 5289

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

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

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 2734  ax-sep 5255

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  ssexi  5291  ssexgOLD  5292  intex  5312  moabexOLD  5438  naddunif  8685  ixpiunwdom  9565  omex  9625  tcss  9724  bndrank  9826  scottex  9875  scottexOLD  9876  aceq3lem  10126  cfslb  10271  dcomex  10452  axdc2lem  10453  grothpw  10838  grothpwex  10839  grothomex  10841  elnp  10999  negfi  12191  limsuple  15567  limsuplt  15568  limsupbnd1  15571  o1add2  15713  o1mul2  15714  o1sub2  15715  o1dif  15719  caucvgrlem  15762  fsumo1  15901  lcmfval  16715  lcmf0val  16716  unbenlem  17004  ressbas2  17334  prdsval  17544  prdsbas  17546  rescbas  17922  reschom  17923  rescco  17925  acsmapd  18646  issstrmgm  18749  issubmgm2  18809  issubmnd  18870  eqgfval  19305  dfod2  19695  ablfac1b  20203  islinds2  22030  pmatcollpw3lem  23012  2basgen  23219  prdstopn  23858  ressust  24493  rectbntr0  25063  elcncf  25121  cncfcnvcn  25157  cmssmscld  25582  cmsss  25583  ovolctb2  25724  limcfval  26104  ellimc2  26109  limcflf  26113  limcres  26118  limcun  26127  dvfval  26129  lhop2  26247  taylfval  26595  ulmval  26616  xrlimcnp  27206  axtgcont1  28810  ressnm  33406  ressprs  33408  ordtrestNEW  34433  ddeval1  34747  ddeval0  34748  carsgclctunlem3  34833  bnj849  35436  msrval  36119  mclsval  36144  brsset  36468  isfne4  36961  refssfne  36979  topjoin  36986  bj-snglex  37719  mblfinlem3  38410  filbcmb  38492  cnpwstotbnd  38549  ismtyval  38552  ispsubsp  40620  ispsubclN  40812  isnumbasgrplem2  43947  rtrclex  44459  brmptiunrelexpd  44525  iunrelexp0  44544  mulcncff  46700  subcncff  46710  addcncff  46714  cncfuni  46716  divcncff  46721  etransclem1  47065  etransclem4  47068  etransclem13  47077  isvonmbl  47468  isubgriedg  48781  isubgrvtx  48785  uhgrimisgrgric  48849  linccl  49346  ellcoellss  49367  elbigolo1  49489