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  18807  issubmnd  18868  eqgfval  19302  dfod2  19692  ablfac1b  20200  islinds2  22027  pmatcollpw3lem  23009  2basgen  23216  prdstopn  23855  ressust  24490  rectbntr0  25060  elcncf  25118  cncfcnvcn  25154  cmssmscld  25579  cmsss  25580  ovolctb2  25721  limcfval  26101  ellimc2  26106  limcflf  26110  limcres  26115  limcun  26124  dvfval  26126  lhop2  26244  taylfval  26592  ulmval  26613  xrlimcnp  27203  axtgcont1  28807  ressnm  33391  ressprs  33393  ordtrestNEW  34418  ddeval1  34732  ddeval0  34733  carsgclctunlem3  34818  bnj849  35421  msrval  36104  mclsval  36129  brsset  36453  isfne4  36946  refssfne  36964  topjoin  36971  bj-snglex  37704  mblfinlem3  38395  filbcmb  38477  cnpwstotbnd  38534  ismtyval  38537  ispsubsp  40605  ispsubclN  40797  isnumbasgrplem2  43932  rtrclex  44444  brmptiunrelexpd  44510  iunrelexp0  44529  mulcncff  46685  subcncff  46695  addcncff  46699  cncfuni  46701  divcncff  46706  etransclem1  47050  etransclem4  47053  etransclem13  47062  isvonmbl  47453  isubgriedg  48766  isubgrvtx  48770  uhgrimisgrgric  48834  linccl  49331  ellcoellss  49352  elbigolo1  49474