Theorem ssex 5322

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∩ cin 3948   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  ssexi  5323  ssexg  5324  intex  5338  moabex  5460  naddunif  8692  ixpiunwdom  9585  omex  9638  tcss  9739  bndrank  9836  scottex  9880  aceq3lem  10115  cfslb  10261  dcomex  10442  axdc2lem  10443  grothpw  10821  grothpwex  10822  grothomex  10824  elnp  10982  negfi  12163  hashfacenOLD  14414  limsuple  15422  limsuplt  15423  limsupbnd1  15426  o1add2  15568  o1mul2  15569  o1sub2  15570  o1dif  15574  caucvgrlem  15619  fsumo1  15758  lcmfval  16558  lcmf0val  16559  unbenlem  16841  ressbas2  17182  prdsval  17401  prdsbas  17403  rescbas  17776  rescbasOLD  17777  reschom  17778  rescco  17780  resccoOLD  17781  acsmapd  18507  issstrmgm  18572  issubmnd  18652  eqgfval  19056  dfod2  19432  ablfac1b  19940  islinds2  21368  pmatcollpw3lem  22285  2basgen  22493  prdstopn  23132  ressust  23768  rectbntr0  24348  elcncf  24405  cncfcnvcn  24441  cmssmscld  24867  cmsss  24868  ovolctb2  25009  limcfval  25389  ellimc2  25394  limcflf  25398  limcres  25403  limcun  25412  dvfval  25414  lhop2  25532  taylfval  25871  ulmval  25892  xrlimcnp  26473  axtgcont1  27719  fpwrelmap  31958  ressnm  32128  ressprs  32133  ordtrestNEW  32901  ddeval1  33232  ddeval0  33233  carsgclctunlem3  33319  bnj849  33936  msrval  34529  mclsval  34554  brsset  34861  isfne4  35225  refssfne  35243  topjoin  35250  bj-snglex  35854  mblfinlem3  36527  filbcmb  36608  cnpwstotbnd  36665  ismtyval  36668  ispsubsp  38616  ispsubclN  38808  isnumbasgrplem2  41846  rtrclex  42368  brmptiunrelexpd  42434  iunrelexp0  42453  mulcncff  44586  subcncff  44596  addcncff  44600  cncfuni  44602  divcncff  44607  etransclem1  44951  etransclem4  44954  etransclem13  44963  isvonmbl  45354  issubmgm2  46560  linccl  47095  ellcoellss  47116  elbigolo1  47243