Theorem ssex 5321

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474   ∩ cin 3947   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  ssexi  5322  ssexg  5323  intex  5337  moabex  5459  naddunif  8691  ixpiunwdom  9584  omex  9637  tcss  9738  bndrank  9835  scottex  9879  aceq3lem  10114  cfslb  10260  dcomex  10441  axdc2lem  10442  grothpw  10820  grothpwex  10821  grothomex  10823  elnp  10981  negfi  12162  hashfacenOLD  14413  limsuple  15421  limsuplt  15422  limsupbnd1  15425  o1add2  15567  o1mul2  15568  o1sub2  15569  o1dif  15573  caucvgrlem  15618  fsumo1  15757  lcmfval  16557  lcmf0val  16558  unbenlem  16840  ressbas2  17181  prdsval  17400  prdsbas  17402  rescbas  17775  rescbasOLD  17776  reschom  17777  rescco  17779  resccoOLD  17780  acsmapd  18506  issstrmgm  18571  issubmnd  18651  eqgfval  19055  dfod2  19431  ablfac1b  19939  islinds2  21367  pmatcollpw3lem  22284  2basgen  22492  prdstopn  23131  ressust  23767  rectbntr0  24347  elcncf  24404  cncfcnvcn  24440  cmssmscld  24866  cmsss  24867  ovolctb2  25008  limcfval  25388  ellimc2  25393  limcflf  25397  limcres  25402  limcun  25411  dvfval  25413  lhop2  25531  taylfval  25870  ulmval  25891  xrlimcnp  26470  axtgcont1  27716  fpwrelmap  31953  ressnm  32123  ressprs  32128  ordtrestNEW  32896  ddeval1  33227  ddeval0  33228  carsgclctunlem3  33314  bnj849  33931  msrval  34524  mclsval  34549  brsset  34856  isfne4  35220  refssfne  35238  topjoin  35245  bj-snglex  35849  mblfinlem3  36522  filbcmb  36603  cnpwstotbnd  36660  ismtyval  36663  ispsubsp  38611  ispsubclN  38803  isnumbasgrplem2  41836  rtrclex  42358  brmptiunrelexpd  42424  iunrelexp0  42443  mulcncff  44576  subcncff  44586  addcncff  44590  cncfuni  44592  divcncff  44597  etransclem1  44941  etransclem4  44944  etransclem13  44953  isvonmbl  45344  issubmgm2  46550  linccl  47085  ellcoellss  47106  elbigolo1  47233