Theorem ssex 5326

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 5301 (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 3980	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5323	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2826	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 233	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  ssexi  5327  ssexg  5328  intex  5349  moabex  5469  naddunif  8729  ixpiunwdom  9627  omex  9680  tcss  9781  bndrank  9878  scottex  9922  aceq3lem  10157  cfslb  10303  dcomex  10484  axdc2lem  10485  grothpw  10863  grothpwex  10864  grothomex  10866  elnp  11024  negfi  12214  limsuple  15510  limsuplt  15511  limsupbnd1  15514  o1add2  15656  o1mul2  15657  o1sub2  15658  o1dif  15662  caucvgrlem  15705  fsumo1  15844  lcmfval  16654  lcmf0val  16655  unbenlem  16941  ressbas2  17282  prdsval  17501  prdsbas  17503  rescbas  17876  rescbasOLD  17877  reschom  17878  rescco  17880  resccoOLD  17881  acsmapd  18611  issstrmgm  18678  issubmgm2  18728  issubmnd  18786  eqgfval  19206  dfod2  19596  ablfac1b  20104  islinds2  21850  pmatcollpw3lem  22804  2basgen  23012  prdstopn  23651  ressust  24287  rectbntr0  24867  elcncf  24928  cncfcnvcn  24965  cmssmscld  25397  cmsss  25398  ovolctb2  25540  limcfval  25921  ellimc2  25926  limcflf  25930  limcres  25935  limcun  25944  dvfval  25946  lhop2  26068  taylfval  26414  ulmval  26437  xrlimcnp  27025  axtgcont1  28490  fpwrelmap  32750  ressnm  32933  ressprs  32938  ordtrestNEW  33881  ddeval1  34214  ddeval0  34215  carsgclctunlem3  34301  bnj849  34917  msrval  35522  mclsval  35547  brsset  35870  isfne4  36322  refssfne  36340  topjoin  36347  bj-snglex  36955  mblfinlem3  37645  filbcmb  37726  cnpwstotbnd  37783  ismtyval  37786  ispsubsp  39727  ispsubclN  39919  isnumbasgrplem2  43092  rtrclex  43606  brmptiunrelexpd  43672  iunrelexp0  43691  mulcncff  45825  subcncff  45835  addcncff  45839  cncfuni  45841  divcncff  45846  etransclem1  46190  etransclem4  46193  etransclem13  46202  isvonmbl  46593  isubgriedg  47786  isubgrvtx  47790  uhgrimisgrgric  47836  linccl  48259  ellcoellss  48280  elbigolo1  48406