Theorem ssex 5281

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  ssexi  5283  ssexgOLD  5284  intex  5304  moabexOLD  5426  naddunif  8703  ixpiunwdom  9584  omex  9644  tcss  9743  bndrank  9854  scottex  9933  scottexOLD  9934  aceq3lem  10199  cfslb  10344  dcomex  10525  axdc2lem  10526  grothpw  10911  grothpwex  10912  grothomex  10914  elnp  11072  negfi  12266  limsuple  15645  limsuplt  15646  limsupbnd1  15649  o1add2  15791  o1mul2  15792  o1sub2  15793  o1dif  15797  caucvgrlem  15840  fsumo1  15979  lcmfval  16796  lcmf0val  16797  unbenlem  17086  ressbas2  17416  prdsval  17626  prdsbas  17628  rescbas  18004  reschom  18005  rescco  18007  acsmapd  18728  issstrmgm  18831  issubmgm2  18892  issubmnd  18953  eqgfval  19388  dfod2  19778  ablfac1b  20286  islinds2  22119  pmatcollpw3lem  23101  2basgen  23308  prdstopn  23947  ressust  24582  rectbntr0  25152  elcncf  25210  cncfcnvcn  25246  cmssmscld  25671  cmsss  25672  ovolctb2  25813  limcfval  26192  ellimc2  26197  limcflf  26201  limcres  26206  limcun  26215  dvfval  26217  lhop2  26335  taylfval  26686  ulmval  26707  xrlimcnp  27296  axtgcont1  28930  ressnm  33525  ressprs  33527  ordtrestNEW  34553  ddeval1  34867  ddeval0  34868  carsgclctunlem3  34952  bnj849  35555  onprcf1acwevdlem1  35895  msrval  36303  mclsval  36328  brsset  36651  isfne4  37128  refssfne  37146  topjoin  37153  bj-snglex  37886  mblfinlem3  38578  filbcmb  38675  cnpwstotbnd  38732  ismtyval  38735  ispsubsp  40803  ispsubclN  40995  isnumbasgrplem2  44106  rtrclex  44617  brmptiunrelexpd  44683  iunrelexp0  44702  mulcncff  46880  subcncff  46890  addcncff  46894  cncfuni  46896  divcncff  46901  etransclem1  47245  etransclem4  47248  etransclem13  47257  isvonmbl  47648  isubgriedg  48961  isubgrvtx  48965  uhgrimisgrgric  49029  linccl  49526  ellcoellss  49547  elbigolo1  49669