Theorem ssex 5279

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 5254 (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 3935	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5276	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2817	. . 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 3450   ∩ cin 3916   ⊆ wss 3917

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  ssexi  5280  ssexg  5281  intex  5302  moabex  5422  naddunif  8660  ixpiunwdom  9550  omex  9603  tcss  9704  bndrank  9801  scottex  9845  aceq3lem  10080  cfslb  10226  dcomex  10407  axdc2lem  10408  grothpw  10786  grothpwex  10787  grothomex  10789  elnp  10947  negfi  12139  limsuple  15451  limsuplt  15452  limsupbnd1  15455  o1add2  15597  o1mul2  15598  o1sub2  15599  o1dif  15603  caucvgrlem  15646  fsumo1  15785  lcmfval  16598  lcmf0val  16599  unbenlem  16886  ressbas2  17215  prdsval  17425  prdsbas  17427  rescbas  17798  reschom  17799  rescco  17801  acsmapd  18520  issstrmgm  18587  issubmgm2  18637  issubmnd  18695  eqgfval  19115  dfod2  19501  ablfac1b  20009  islinds2  21729  pmatcollpw3lem  22677  2basgen  22884  prdstopn  23522  ressust  24158  rectbntr0  24728  elcncf  24789  cncfcnvcn  24826  cmssmscld  25257  cmsss  25258  ovolctb2  25400  limcfval  25780  ellimc2  25785  limcflf  25789  limcres  25794  limcun  25803  dvfval  25805  lhop2  25927  taylfval  26273  ulmval  26296  xrlimcnp  26885  axtgcont1  28402  fpwrelmap  32663  ressnm  32893  ressprs  32897  ordtrestNEW  33918  ddeval1  34231  ddeval0  34232  carsgclctunlem3  34318  bnj849  34922  msrval  35532  mclsval  35557  brsset  35884  isfne4  36335  refssfne  36353  topjoin  36360  bj-snglex  36968  mblfinlem3  37660  filbcmb  37741  cnpwstotbnd  37798  ismtyval  37801  ispsubsp  39746  ispsubclN  39938  isnumbasgrplem2  43100  rtrclex  43613  brmptiunrelexpd  43679  iunrelexp0  43698  mulcncff  45875  subcncff  45885  addcncff  45889  cncfuni  45891  divcncff  45896  etransclem1  46240  etransclem4  46243  etransclem13  46252  isvonmbl  46643  isubgriedg  47867  isubgrvtx  47871  uhgrimisgrgric  47935  linccl  48407  ellcoellss  48428  elbigolo1  48550