Theorem ssex 5265

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3439   ∩ cin 3899   ⊆ wss 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-in 3907  df-ss 3917

This theorem is referenced by:  ssexi  5266  ssexg  5267  intex  5288  moabexOLD  5406  naddunif  8621  ixpiunwdom  9497  omex  9554  tcss  9653  bndrank  9755  scottex  9799  aceq3lem  10032  cfslb  10178  dcomex  10359  axdc2lem  10360  grothpw  10739  grothpwex  10740  grothomex  10742  elnp  10900  negfi  12093  limsuple  15403  limsuplt  15404  limsupbnd1  15407  o1add2  15549  o1mul2  15550  o1sub2  15551  o1dif  15555  caucvgrlem  15598  fsumo1  15737  lcmfval  16550  lcmf0val  16551  unbenlem  16838  ressbas2  17167  prdsval  17377  prdsbas  17379  rescbas  17755  reschom  17756  rescco  17758  acsmapd  18479  issstrmgm  18580  issubmgm2  18630  issubmnd  18688  eqgfval  19107  dfod2  19495  ablfac1b  20003  islinds2  21770  pmatcollpw3lem  22729  2basgen  22936  prdstopn  23574  ressust  24209  rectbntr0  24779  elcncf  24840  cncfcnvcn  24877  cmssmscld  25308  cmsss  25309  ovolctb2  25451  limcfval  25831  ellimc2  25836  limcflf  25840  limcres  25845  limcun  25854  dvfval  25856  lhop2  25978  taylfval  26324  ulmval  26347  xrlimcnp  26936  axtgcont1  28521  ressnm  33025  ressprs  33027  ordtrestNEW  34057  ddeval1  34370  ddeval0  34371  carsgclctunlem3  34456  bnj849  35060  msrval  35711  mclsval  35736  brsset  36060  isfne4  36513  refssfne  36531  topjoin  36538  bj-snglex  37147  mblfinlem3  37829  filbcmb  37910  cnpwstotbnd  37967  ismtyval  37970  ispsubsp  40040  ispsubclN  40232  isnumbasgrplem2  43383  rtrclex  43895  brmptiunrelexpd  43961  iunrelexp0  43980  mulcncff  46151  subcncff  46161  addcncff  46165  cncfuni  46167  divcncff  46172  etransclem1  46516  etransclem4  46519  etransclem13  46528  isvonmbl  46919  isubgriedg  48146  isubgrvtx  48150  uhgrimisgrgric  48214  linccl  48697  ellcoellss  48718  elbigolo1  48840