Theorem ssex 5252

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 5221 (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 3903	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5249	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2829	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 235	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 219	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121  Vcvv 3433   ∩ cin 3884   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902

This theorem is referenced by:  ssexi  5253  ssexg  5254  intex  5275  moabexOLD  5401  naddunif  8623  ixpiunwdom  9499  omex  9559  tcss  9658  bndrank  9760  scottex  9804  aceq3lem  10037  cfslb  10183  dcomex  10364  axdc2lem  10365  grothpw  10744  grothpwex  10745  grothomex  10747  elnp  10905  negfi  12100  limsuple  15435  limsuplt  15436  limsupbnd1  15439  o1add2  15581  o1mul2  15582  o1sub2  15583  o1dif  15587  caucvgrlem  15630  fsumo1  15770  lcmfval  16585  lcmf0val  16586  unbenlem  16874  ressbas2  17203  prdsval  17413  prdsbas  17415  rescbas  17791  reschom  17792  rescco  17794  acsmapd  18515  issstrmgm  18616  issubmgm2  18666  issubmnd  18724  eqgfval  19146  dfod2  19534  ablfac1b  20042  islinds2  21792  pmatcollpw3lem  22770  2basgen  22977  prdstopn  23615  ressust  24250  rectbntr0  24820  elcncf  24878  cncfcnvcn  24914  cmssmscld  25339  cmsss  25340  ovolctb2  25481  limcfval  25861  ellimc2  25866  limcflf  25870  limcres  25875  limcun  25884  dvfval  25886  lhop2  26004  taylfval  26346  ulmval  26367  xrlimcnp  26954  axtgcont1  28558  ressnm  33047  ressprs  33049  ordtrestNEW  34117  ddeval1  34430  ddeval0  34431  carsgclctunlem3  34516  bnj849  35122  msrval  35781  mclsval  35806  brsset  36130  isfne4  36583  refssfne  36601  topjoin  36608  bj-snglex  37341  mblfinlem3  38041  filbcmb  38122  cnpwstotbnd  38179  ismtyval  38182  ispsubsp  40252  ispsubclN  40444  isnumbasgrplem2  43564  rtrclex  44076  brmptiunrelexpd  44142  iunrelexp0  44161  mulcncff  46327  subcncff  46337  addcncff  46341  cncfuni  46343  divcncff  46348  etransclem1  46692  etransclem4  46695  etransclem13  46704  isvonmbl  47095  isubgriedg  48368  isubgrvtx  48372  uhgrimisgrgric  48436  linccl  48919  ellcoellss  48940  elbigolo1  49062