Theorem ssex 5270

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 5245 (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 5267	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2825	. . 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 3442   ∩ cin 3902   ⊆ wss 3903

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 2709  ax-sep 5245

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  ssexi  5271  ssexg  5272  intex  5293  moabexOLD  5416  naddunif  8633  ixpiunwdom  9509  omex  9566  tcss  9665  bndrank  9767  scottex  9811  aceq3lem  10044  cfslb  10190  dcomex  10371  axdc2lem  10372  grothpw  10751  grothpwex  10752  grothomex  10754  elnp  10912  negfi  12105  limsuple  15415  limsuplt  15416  limsupbnd1  15419  o1add2  15561  o1mul2  15562  o1sub2  15563  o1dif  15567  caucvgrlem  15610  fsumo1  15749  lcmfval  16562  lcmf0val  16563  unbenlem  16850  ressbas2  17179  prdsval  17389  prdsbas  17391  rescbas  17767  reschom  17768  rescco  17770  acsmapd  18491  issstrmgm  18592  issubmgm2  18642  issubmnd  18700  eqgfval  19122  dfod2  19510  ablfac1b  20018  islinds2  21785  pmatcollpw3lem  22744  2basgen  22951  prdstopn  23589  ressust  24224  rectbntr0  24794  elcncf  24855  cncfcnvcn  24892  cmssmscld  25323  cmsss  25324  ovolctb2  25466  limcfval  25846  ellimc2  25851  limcflf  25855  limcres  25860  limcun  25869  dvfval  25871  lhop2  25993  taylfval  26339  ulmval  26362  xrlimcnp  26951  axtgcont1  28558  ressnm  33063  ressprs  33065  ordtrestNEW  34105  ddeval1  34418  ddeval0  34419  carsgclctunlem3  34504  bnj849  35107  msrval  35760  mclsval  35785  brsset  36109  isfne4  36562  refssfne  36580  topjoin  36587  bj-snglex  37248  mblfinlem3  37939  filbcmb  38020  cnpwstotbnd  38077  ismtyval  38080  ispsubsp  40150  ispsubclN  40342  isnumbasgrplem2  43490  rtrclex  44002  brmptiunrelexpd  44068  iunrelexp0  44087  mulcncff  46257  subcncff  46267  addcncff  46271  cncfuni  46273  divcncff  46278  etransclem1  46622  etransclem4  46625  etransclem13  46634  isvonmbl  47025  isubgriedg  48252  isubgrvtx  48256  uhgrimisgrgric  48320  linccl  48803  ellcoellss  48824  elbigolo1  48946