Theorem ssex 5227

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 5205 (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		df-ss 3954	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5224	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2902	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 235	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 219	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3496   ∩ cin 3937   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954

This theorem is referenced by:  ssexi  5228  ssexg  5229  intex  5242  moabex  5353  ixpiunwdom  9057  omex  9108  tcss  9188  bndrank  9272  scottex  9316  aceq3lem  9548  cfslb  9690  dcomex  9871  axdc2lem  9872  grothpw  10250  grothpwex  10251  grothomex  10253  elnp  10411  negfi  11591  hashfacen  13815  limsuple  14837  limsuplt  14838  limsupbnd1  14841  o1add2  14982  o1mul2  14983  o1sub2  14984  o1dif  14988  caucvgrlem  15031  fsumo1  15169  lcmfval  15967  lcmf0val  15968  unbenlem  16246  ressbas2  16557  prdsval  16730  prdsbas  16732  rescbas  17101  reschom  17102  rescco  17104  acsmapd  17790  issstrmgm  17865  issubmnd  17940  eqgfval  18330  dfod2  18693  ablfac1b  19194  islinds2  20959  pmatcollpw3lem  21393  2basgen  21600  prdstopn  22238  ressust  22875  rectbntr0  23442  elcncf  23499  cncfcnvcn  23531  cmssmscld  23955  cmsss  23956  ovolctb2  24095  limcfval  24472  ellimc2  24477  limcflf  24481  limcres  24486  limcun  24495  dvfval  24497  lhop2  24614  taylfval  24949  ulmval  24970  xrlimcnp  25548  axtgcont1  26256  fpwrelmap  30471  ressnm  30640  ressprs  30644  ordtrestNEW  31166  ddeval1  31495  ddeval0  31496  carsgclctunlem3  31580  bnj849  32199  msrval  32787  mclsval  32812  brsset  33352  isfne4  33690  refssfne  33708  topjoin  33715  bj-snglex  34287  mblfinlem3  34933  filbcmb  35017  cnpwstotbnd  35077  ismtyval  35080  ispsubsp  36883  ispsubclN  37075  isnumbasgrplem2  39711  rtrclex  39984  brmptiunrelexpd  40035  iunrelexp0  40054  mulcncff  42158  subcncff  42170  addcncff  42174  cncfuni  42176  divcncff  42181  etransclem1  42527  etransclem4  42530  etransclem13  42539  isvonmbl  42927  issubmgm2  44064  linccl  44476  ellcoellss  44497  elbigolo1  44624