Theorem ssex 5260

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∩ cin 3902   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  ssexi  5261  ssexg  5262  intex  5283  moabex  5402  naddunif  8611  ixpiunwdom  9482  omex  9539  tcss  9640  bndrank  9737  scottex  9781  aceq3lem  10014  cfslb  10160  dcomex  10341  axdc2lem  10342  grothpw  10720  grothpwex  10721  grothomex  10723  elnp  10881  negfi  12074  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  18527  issubmgm2  18577  issubmnd  18635  eqgfval  19055  dfod2  19443  ablfac1b  19951  islinds2  21720  pmatcollpw3lem  22668  2basgen  22875  prdstopn  23513  ressust  24149  rectbntr0  24719  elcncf  24780  cncfcnvcn  24817  cmssmscld  25248  cmsss  25249  ovolctb2  25391  limcfval  25771  ellimc2  25776  limcflf  25780  limcres  25785  limcun  25794  dvfval  25796  lhop2  25918  taylfval  26264  ulmval  26287  xrlimcnp  26876  axtgcont1  28417  fpwrelmap  32685  ressnm  32915  ressprs  32917  ordtrestNEW  33904  ddeval1  34217  ddeval0  34218  carsgclctunlem3  34304  bnj849  34908  msrval  35531  mclsval  35556  brsset  35883  isfne4  36334  refssfne  36352  topjoin  36359  bj-snglex  36967  mblfinlem3  37659  filbcmb  37740  cnpwstotbnd  37797  ismtyval  37800  ispsubsp  39744  ispsubclN  39936  isnumbasgrplem2  43097  rtrclex  43610  brmptiunrelexpd  43676  iunrelexp0  43695  mulcncff  45871  subcncff  45881  addcncff  45885  cncfuni  45887  divcncff  45892  etransclem1  46236  etransclem4  46239  etransclem13  46248  isvonmbl  46639  isubgriedg  47867  isubgrvtx  47871  uhgrimisgrgric  47935  linccl  48419  ellcoellss  48440  elbigolo1  48562