Theorem ssex 5286

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  ssexi  5288  ssexgOLD  5289  intex  5309  moabexOLD  5431  naddunif  8728  ixpiunwdom  9608  omex  9668  tcss  9767  bndrank  9878  scottex  9957  scottexOLD  9958  aceq3lem  10223  cfslb  10368  dcomex  10549  axdc2lem  10550  grothpw  10935  grothpwex  10936  grothomex  10938  elnp  11096  negfi  12290  limsuple  15671  limsuplt  15672  limsupbnd1  15675  o1add2  15817  o1mul2  15818  o1sub2  15819  o1dif  15823  caucvgrlem  15866  fsumo1  16005  lcmfval  16822  lcmf0val  16823  unbenlem  17112  ressbas2  17442  prdsval  17652  prdsbas  17654  rescbas  18030  reschom  18031  rescco  18033  acsmapd  18754  issstrmgm  18857  issubmgm2  18918  issubmnd  18979  eqgfval  19414  dfod2  19805  ablfac1b  20313  islinds2  22146  pmatcollpw3lem  23128  2basgen  23335  prdstopn  23974  ressust  24609  rectbntr0  25179  elcncf  25237  cncfcnvcn  25273  cmssmscld  25698  cmsss  25699  ovolctb2  25840  limcfval  26219  ellimc2  26224  limcflf  26228  limcres  26233  limcun  26242  dvfval  26244  lhop2  26362  taylfval  26713  ulmval  26734  xrlimcnp  27323  axtgcont1  28957  ressnm  33592  ressprs  33594  ordtrestNEW  34620  ddeval1  34934  ddeval0  34935  carsgclctunlem3  35019  bnj849  35622  onprcf1acwevdlem1  36044  msrval  36469  mclsval  36494  brsset  36828  isfne4  37305  refssfne  37323  topjoin  37330  bj-snglex  38063  mblfinlem3  38768  filbcmb  38865  cnpwstotbnd  38922  ismtyval  38925  ispsubsp  40993  ispsubclN  41185  isnumbasgrplem2  44296  rtrclex  44807  brmptiunrelexpd  44873  iunrelexp0  44892  mulcncff  47083  subcncff  47093  addcncff  47097  cncfuni  47099  divcncff  47104  etransclem1  47448  etransclem4  47451  etransclem13  47460  isvonmbl  47851  isubgriedg  49164  isubgrvtx  49168  uhgrimisgrgric  49232  linccl  49729  ellcoellss  49750  elbigolo1  49872