Theorem ssex 5271

Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 5246 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
ssex.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ssex	⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Proof of Theorem ssex

Step	Hyp	Ref	Expression
1		dfss2 3929	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5268	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2816	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 233	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  ssexi  5272  ssexg  5273  intex  5294  moabex  5414  naddunif  8634  ixpiunwdom  9519  omex  9574  tcss  9675  bndrank  9772  scottex  9816  aceq3lem  10051  cfslb  10197  dcomex  10378  axdc2lem  10379  grothpw  10757  grothpwex  10758  grothomex  10760  elnp  10918  negfi  12110  limsuple  15421  limsuplt  15422  limsupbnd1  15425  o1add2  15567  o1mul2  15568  o1sub2  15569  o1dif  15573  caucvgrlem  15616  fsumo1  15755  lcmfval  16568  lcmf0val  16569  unbenlem  16856  ressbas2  17185  prdsval  17395  prdsbas  17397  rescbas  17772  reschom  17773  rescco  17775  acsmapd  18496  issstrmgm  18563  issubmgm2  18613  issubmnd  18671  eqgfval  19091  dfod2  19479  ablfac1b  19987  islinds2  21756  pmatcollpw3lem  22704  2basgen  22911  prdstopn  23549  ressust  24185  rectbntr0  24755  elcncf  24816  cncfcnvcn  24853  cmssmscld  25284  cmsss  25285  ovolctb2  25427  limcfval  25807  ellimc2  25812  limcflf  25816  limcres  25821  limcun  25830  dvfval  25832  lhop2  25954  taylfval  26300  ulmval  26323  xrlimcnp  26912  axtgcont1  28449  fpwrelmap  32707  ressnm  32937  ressprs  32939  ordtrestNEW  33905  ddeval1  34218  ddeval0  34219  carsgclctunlem3  34305  bnj849  34909  msrval  35519  mclsval  35544  brsset  35871  isfne4  36322  refssfne  36340  topjoin  36347  bj-snglex  36955  mblfinlem3  37647  filbcmb  37728  cnpwstotbnd  37785  ismtyval  37788  ispsubsp  39733  ispsubclN  39925  isnumbasgrplem2  43087  rtrclex  43600  brmptiunrelexpd  43666  iunrelexp0  43685  mulcncff  45862  subcncff  45872  addcncff  45876  cncfuni  45878  divcncff  45883  etransclem1  46227  etransclem4  46230  etransclem13  46239  isvonmbl  46630  isubgriedg  47857  isubgrvtx  47861  uhgrimisgrgric  47925  linccl  48397  ellcoellss  48418  elbigolo1  48540