Theorem ssex 5251

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 5220 (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 5248	. . 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 3427   ∩ cin 3884   ⊆ wss 3885

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 5220

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 3388  df-v 3429  df-in 3892  df-ss 3902

This theorem is referenced by:  ssexi  5252  ssexg  5253  intex  5274  moabexOLD  5400  naddunif  8618  ixpiunwdom  9494  omex  9553  tcss  9652  bndrank  9754  scottex  9798  aceq3lem  10031  cfslb  10177  dcomex  10358  axdc2lem  10359  grothpw  10738  grothpwex  10739  grothomex  10741  elnp  10899  negfi  12094  limsuple  15429  limsuplt  15430  limsupbnd1  15433  o1add2  15575  o1mul2  15576  o1sub2  15577  o1dif  15581  caucvgrlem  15624  fsumo1  15764  lcmfval  16579  lcmf0val  16580  unbenlem  16868  ressbas2  17197  prdsval  17407  prdsbas  17409  rescbas  17785  reschom  17786  rescco  17788  acsmapd  18509  issstrmgm  18610  issubmgm2  18660  issubmnd  18718  eqgfval  19140  dfod2  19528  ablfac1b  20036  islinds2  21782  pmatcollpw3lem  22736  2basgen  22943  prdstopn  23581  ressust  24216  rectbntr0  24786  elcncf  24844  cncfcnvcn  24880  cmssmscld  25305  cmsss  25306  ovolctb2  25447  limcfval  25827  ellimc2  25832  limcflf  25836  limcres  25841  limcun  25850  dvfval  25852  lhop2  25970  taylfval  26312  ulmval  26333  xrlimcnp  26920  axtgcont1  28524  ressnm  33012  ressprs  33014  ordtrestNEW  34053  ddeval1  34366  ddeval0  34367  carsgclctunlem3  34452  bnj849  35055  msrval  35708  mclsval  35733  brsset  36057  isfne4  36510  refssfne  36528  topjoin  36535  bj-snglex  37268  mblfinlem3  37968  filbcmb  38049  cnpwstotbnd  38106  ismtyval  38109  ispsubsp  40179  ispsubclN  40371  isnumbasgrplem2  43520  rtrclex  44032  brmptiunrelexpd  44098  iunrelexp0  44117  mulcncff  46286  subcncff  46296  addcncff  46300  cncfuni  46302  divcncff  46307  etransclem1  46651  etransclem4  46654  etransclem13  46663  isvonmbl  47054  isubgriedg  48327  isubgrvtx  48331  uhgrimisgrgric  48395  linccl  48878  ellcoellss  48899  elbigolo1  49021