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  8635  ixpiunwdom  9520  omex  9575  tcss  9676  bndrank  9773  scottex  9817  aceq3lem  10052  cfslb  10198  dcomex  10379  axdc2lem  10380  grothpw  10758  grothpwex  10759  grothomex  10761  elnp  10919  negfi  12111  limsuple  15422  limsuplt  15423  limsupbnd1  15426  o1add2  15568  o1mul2  15569  o1sub2  15570  o1dif  15574  caucvgrlem  15617  fsumo1  15756  lcmfval  16569  lcmf0val  16570  unbenlem  16857  ressbas2  17186  prdsval  17396  prdsbas  17398  rescbas  17773  reschom  17774  rescco  17776  acsmapd  18497  issstrmgm  18564  issubmgm2  18614  issubmnd  18672  eqgfval  19092  dfod2  19480  ablfac1b  19988  islinds2  21757  pmatcollpw3lem  22705  2basgen  22912  prdstopn  23550  ressust  24186  rectbntr0  24756  elcncf  24817  cncfcnvcn  24854  cmssmscld  25285  cmsss  25286  ovolctb2  25428  limcfval  25808  ellimc2  25813  limcflf  25817  limcres  25822  limcun  25831  dvfval  25833  lhop2  25955  taylfval  26301  ulmval  26324  xrlimcnp  26913  axtgcont1  28450  fpwrelmap  32708  ressnm  32938  ressprs  32940  ordtrestNEW  33906  ddeval1  34219  ddeval0  34220  carsgclctunlem3  34306  bnj849  34910  msrval  35520  mclsval  35545  brsset  35872  isfne4  36323  refssfne  36341  topjoin  36348  bj-snglex  36956  mblfinlem3  37648  filbcmb  37729  cnpwstotbnd  37786  ismtyval  37789  ispsubsp  39734  ispsubclN  39926  isnumbasgrplem2  43088  rtrclex  43601  brmptiunrelexpd  43667  iunrelexp0  43686  mulcncff  45863  subcncff  45873  addcncff  45877  cncfuni  45879  divcncff  45884  etransclem1  46228  etransclem4  46231  etransclem13  46240  isvonmbl  46631  isubgriedg  47858  isubgrvtx  47862  uhgrimisgrgric  47926  linccl  48398  ellcoellss  48419  elbigolo1  48541