Theorem ssex 5339

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  ssexi  5340  ssexg  5341  intex  5362  moabex  5479  naddunif  8749  ixpiunwdom  9659  omex  9712  tcss  9813  bndrank  9910  scottex  9954  aceq3lem  10189  cfslb  10335  dcomex  10516  axdc2lem  10517  grothpw  10895  grothpwex  10896  grothomex  10898  elnp  11056  negfi  12244  limsuple  15524  limsuplt  15525  limsupbnd1  15528  o1add2  15670  o1mul2  15671  o1sub2  15672  o1dif  15676  caucvgrlem  15721  fsumo1  15860  lcmfval  16668  lcmf0val  16669  unbenlem  16955  ressbas2  17296  prdsval  17515  prdsbas  17517  rescbas  17890  rescbasOLD  17891  reschom  17892  rescco  17894  resccoOLD  17895  acsmapd  18624  issstrmgm  18691  issubmgm2  18741  issubmnd  18799  eqgfval  19216  dfod2  19606  ablfac1b  20114  islinds2  21856  pmatcollpw3lem  22810  2basgen  23018  prdstopn  23657  ressust  24293  rectbntr0  24873  elcncf  24934  cncfcnvcn  24971  cmssmscld  25403  cmsss  25404  ovolctb2  25546  limcfval  25927  ellimc2  25932  limcflf  25936  limcres  25941  limcun  25950  dvfval  25952  lhop2  26074  taylfval  26418  ulmval  26441  xrlimcnp  27029  axtgcont1  28494  fpwrelmap  32747  ressnm  32931  ressprs  32936  ordtrestNEW  33867  ddeval1  34198  ddeval0  34199  carsgclctunlem3  34285  bnj849  34901  msrval  35506  mclsval  35531  brsset  35853  isfne4  36306  refssfne  36324  topjoin  36331  bj-snglex  36939  mblfinlem3  37619  filbcmb  37700  cnpwstotbnd  37757  ismtyval  37760  ispsubsp  39702  ispsubclN  39894  isnumbasgrplem2  43061  rtrclex  43579  brmptiunrelexpd  43645  iunrelexp0  43664  mulcncff  45791  subcncff  45801  addcncff  45805  cncfuni  45807  divcncff  45812  etransclem1  46156  etransclem4  46159  etransclem13  46168  isvonmbl  46559  isubgriedg  47735  isubgrvtx  47737  uhgrimisgrgric  47783  linccl  48143  ellcoellss  48164  elbigolo1  48291