Theorem ssex 5291

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∩ cin 3925   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  ssexi  5292  ssexg  5293  intex  5314  moabex  5434  naddunif  8703  ixpiunwdom  9602  omex  9655  tcss  9756  bndrank  9853  scottex  9897  aceq3lem  10132  cfslb  10278  dcomex  10459  axdc2lem  10460  grothpw  10838  grothpwex  10839  grothomex  10841  elnp  10999  negfi  12189  limsuple  15492  limsuplt  15493  limsupbnd1  15496  o1add2  15638  o1mul2  15639  o1sub2  15640  o1dif  15644  caucvgrlem  15687  fsumo1  15826  lcmfval  16638  lcmf0val  16639  unbenlem  16926  ressbas2  17257  prdsval  17467  prdsbas  17469  rescbas  17840  reschom  17841  rescco  17843  acsmapd  18562  issstrmgm  18629  issubmgm2  18679  issubmnd  18737  eqgfval  19157  dfod2  19543  ablfac1b  20051  islinds2  21771  pmatcollpw3lem  22719  2basgen  22926  prdstopn  23564  ressust  24200  rectbntr0  24770  elcncf  24831  cncfcnvcn  24868  cmssmscld  25300  cmsss  25301  ovolctb2  25443  limcfval  25823  ellimc2  25828  limcflf  25832  limcres  25837  limcun  25846  dvfval  25848  lhop2  25970  taylfval  26316  ulmval  26339  xrlimcnp  26928  axtgcont1  28393  fpwrelmap  32656  ressnm  32886  ressprs  32890  ordtrestNEW  33898  ddeval1  34211  ddeval0  34212  carsgclctunlem3  34298  bnj849  34902  msrval  35506  mclsval  35531  brsset  35853  isfne4  36304  refssfne  36322  topjoin  36329  bj-snglex  36937  mblfinlem3  37629  filbcmb  37710  cnpwstotbnd  37767  ismtyval  37770  ispsubsp  39710  ispsubclN  39902  isnumbasgrplem2  43075  rtrclex  43588  brmptiunrelexpd  43654  iunrelexp0  43673  mulcncff  45847  subcncff  45857  addcncff  45861  cncfuni  45863  divcncff  45868  etransclem1  46212  etransclem4  46215  etransclem13  46224  isvonmbl  46615  isubgriedg  47824  isubgrvtx  47828  uhgrimisgrgric  47892  linccl  48338  ellcoellss  48359  elbigolo1  48485