Theorem ssex 5240

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssexi  5241  ssexg  5242  intex  5256  moabex  5368  ixpiunwdom  9279  omex  9331  tcss  9433  bndrank  9530  scottex  9574  aceq3lem  9807  cfslb  9953  dcomex  10134  axdc2lem  10135  grothpw  10513  grothpwex  10514  grothomex  10516  elnp  10674  negfi  11854  hashfacenOLD  14095  limsuple  15115  limsuplt  15116  limsupbnd1  15119  o1add2  15261  o1mul2  15262  o1sub2  15263  o1dif  15267  caucvgrlem  15312  fsumo1  15452  lcmfval  16254  lcmf0val  16255  unbenlem  16537  ressbas2  16875  prdsval  17083  prdsbas  17085  rescbas  17458  rescbasOLD  17459  reschom  17460  rescco  17462  resccoOLD  17463  acsmapd  18187  issstrmgm  18252  issubmnd  18327  eqgfval  18719  dfod2  19086  ablfac1b  19588  islinds2  20930  pmatcollpw3lem  21840  2basgen  22048  prdstopn  22687  ressust  23323  rectbntr0  23901  elcncf  23958  cncfcnvcn  23994  cmssmscld  24419  cmsss  24420  ovolctb2  24561  limcfval  24941  ellimc2  24946  limcflf  24950  limcres  24955  limcun  24964  dvfval  24966  lhop2  25084  taylfval  25423  ulmval  25444  xrlimcnp  26023  axtgcont1  26733  fpwrelmap  30970  ressnm  31138  ressprs  31143  ordtrestNEW  31773  ddeval1  32102  ddeval0  32103  carsgclctunlem3  32187  bnj849  32805  msrval  33400  mclsval  33425  brsset  34118  isfne4  34456  refssfne  34474  topjoin  34481  bj-snglex  35090  mblfinlem3  35743  filbcmb  35825  cnpwstotbnd  35882  ismtyval  35885  ispsubsp  37686  ispsubclN  37878  isnumbasgrplem2  40845  rtrclex  41114  brmptiunrelexpd  41180  iunrelexp0  41199  mulcncff  43301  subcncff  43311  addcncff  43315  cncfuni  43317  divcncff  43322  etransclem1  43666  etransclem4  43669  etransclem13  43678  isvonmbl  44066  issubmgm2  45232  linccl  45643  ellcoellss  45664  elbigolo1  45791