Theorem ssex 5257

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896   ⊆ wss 3897

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  ssexi  5258  ssexg  5259  intex  5280  moabex  5397  naddunif  8608  ixpiunwdom  9476  omex  9533  tcss  9632  bndrank  9734  scottex  9778  aceq3lem  10011  cfslb  10157  dcomex  10338  axdc2lem  10339  grothpw  10717  grothpwex  10718  grothomex  10720  elnp  10878  negfi  12071  limsuple  15385  limsuplt  15386  limsupbnd1  15389  o1add2  15531  o1mul2  15532  o1sub2  15533  o1dif  15537  caucvgrlem  15580  fsumo1  15719  lcmfval  16532  lcmf0val  16533  unbenlem  16820  ressbas2  17149  prdsval  17359  prdsbas  17361  rescbas  17736  reschom  17737  rescco  17739  acsmapd  18460  issstrmgm  18561  issubmgm2  18611  issubmnd  18669  eqgfval  19088  dfod2  19476  ablfac1b  19984  islinds2  21750  pmatcollpw3lem  22698  2basgen  22905  prdstopn  23543  ressust  24178  rectbntr0  24748  elcncf  24809  cncfcnvcn  24846  cmssmscld  25277  cmsss  25278  ovolctb2  25420  limcfval  25800  ellimc2  25805  limcflf  25809  limcres  25814  limcun  25823  dvfval  25825  lhop2  25947  taylfval  26293  ulmval  26316  xrlimcnp  26905  axtgcont1  28446  fpwrelmap  32716  ressnm  32945  ressprs  32947  ordtrestNEW  33934  ddeval1  34247  ddeval0  34248  carsgclctunlem3  34333  bnj849  34937  msrval  35582  mclsval  35607  brsset  35931  isfne4  36384  refssfne  36402  topjoin  36409  bj-snglex  37017  mblfinlem3  37698  filbcmb  37779  cnpwstotbnd  37836  ismtyval  37839  ispsubsp  39843  ispsubclN  40035  isnumbasgrplem2  43196  rtrclex  43709  brmptiunrelexpd  43775  iunrelexp0  43794  mulcncff  45967  subcncff  45977  addcncff  45981  cncfuni  45983  divcncff  45988  etransclem1  46332  etransclem4  46335  etransclem13  46344  isvonmbl  46735  isubgriedg  47962  isubgrvtx  47966  uhgrimisgrgric  48030  linccl  48514  ellcoellss  48535  elbigolo1  48657