Theorem ssex 5318

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 5296 (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 3966	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5315	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2814	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 232	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 216	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  Vcvv 3464   ∩ cin 3947   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5296

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3421  df-v 3466  df-in 3955  df-ss 3965

This theorem is referenced by:  ssexi  5319  ssexg  5320  intex  5336  moabex  5457  naddunif  8714  ixpiunwdom  9625  omex  9678  tcss  9779  bndrank  9876  scottex  9920  aceq3lem  10155  cfslb  10299  dcomex  10480  axdc2lem  10481  grothpw  10859  grothpwex  10860  grothomex  10862  elnp  11020  negfi  12208  hashfacenOLD  14466  limsuple  15474  limsuplt  15475  limsupbnd1  15478  o1add2  15620  o1mul2  15621  o1sub2  15622  o1dif  15626  caucvgrlem  15671  fsumo1  15810  lcmfval  16616  lcmf0val  16617  unbenlem  16904  ressbas2  17245  prdsval  17464  prdsbas  17466  rescbas  17839  rescbasOLD  17840  reschom  17841  rescco  17843  resccoOLD  17844  acsmapd  18573  issstrmgm  18640  issubmgm2  18690  issubmnd  18748  eqgfval  19165  dfod2  19557  ablfac1b  20065  islinds2  21806  pmatcollpw3lem  22772  2basgen  22980  prdstopn  23619  ressust  24255  rectbntr0  24835  elcncf  24896  cncfcnvcn  24933  cmssmscld  25365  cmsss  25366  ovolctb2  25508  limcfval  25888  ellimc2  25893  limcflf  25897  limcres  25902  limcun  25911  dvfval  25913  lhop2  26035  taylfval  26382  ulmval  26405  xrlimcnp  26992  axtgcont1  28391  fpwrelmap  32646  ressnm  32830  ressprs  32835  ordtrestNEW  33748  ddeval1  34079  ddeval0  34080  carsgclctunlem3  34166  bnj849  34782  msrval  35378  mclsval  35403  brsset  35725  isfne4  36064  refssfne  36082  topjoin  36089  bj-snglex  36692  mblfinlem3  37372  filbcmb  37453  cnpwstotbnd  37510  ismtyval  37513  ispsubsp  39456  ispsubclN  39648  isnumbasgrplem2  42801  rtrclex  43320  brmptiunrelexpd  43386  iunrelexp0  43405  mulcncff  45526  subcncff  45536  addcncff  45540  cncfuni  45542  divcncff  45547  etransclem1  45891  etransclem4  45894  etransclem13  45903  isvonmbl  46294  isubgriedg  47465  isubgrvtx  47467  uhgrimisgrgric  47513  linccl  47832  ellcoellss  47853  elbigolo1  47980