Theorem ssex 5319

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3479   ∩ cin 3949   ⊆ wss 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-in 3957  df-ss 3967

This theorem is referenced by:  ssexi  5320  ssexg  5321  intex  5342  moabex  5462  naddunif  8727  ixpiunwdom  9626  omex  9679  tcss  9780  bndrank  9877  scottex  9921  aceq3lem  10156  cfslb  10302  dcomex  10483  axdc2lem  10484  grothpw  10862  grothpwex  10863  grothomex  10865  elnp  11023  negfi  12213  limsuple  15510  limsuplt  15511  limsupbnd1  15514  o1add2  15656  o1mul2  15657  o1sub2  15658  o1dif  15662  caucvgrlem  15705  fsumo1  15844  lcmfval  16654  lcmf0val  16655  unbenlem  16942  ressbas2  17279  prdsval  17496  prdsbas  17498  rescbas  17869  reschom  17870  rescco  17872  acsmapd  18595  issstrmgm  18662  issubmgm2  18712  issubmnd  18770  eqgfval  19190  dfod2  19578  ablfac1b  20086  islinds2  21825  pmatcollpw3lem  22779  2basgen  22987  prdstopn  23626  ressust  24262  rectbntr0  24844  elcncf  24905  cncfcnvcn  24942  cmssmscld  25374  cmsss  25375  ovolctb2  25517  limcfval  25897  ellimc2  25902  limcflf  25906  limcres  25911  limcun  25920  dvfval  25922  lhop2  26044  taylfval  26390  ulmval  26413  xrlimcnp  27001  axtgcont1  28466  fpwrelmap  32733  ressnm  32936  ressprs  32941  ordtrestNEW  33898  ddeval1  34213  ddeval0  34214  carsgclctunlem3  34300  bnj849  34917  msrval  35521  mclsval  35546  brsset  35868  isfne4  36319  refssfne  36337  topjoin  36344  bj-snglex  36952  mblfinlem3  37644  filbcmb  37725  cnpwstotbnd  37782  ismtyval  37785  ispsubsp  39725  ispsubclN  39917  isnumbasgrplem2  43094  rtrclex  43608  brmptiunrelexpd  43674  iunrelexp0  43693  mulcncff  45861  subcncff  45871  addcncff  45875  cncfuni  45877  divcncff  45882  etransclem1  46226  etransclem4  46229  etransclem13  46238  isvonmbl  46629  isubgriedg  47825  isubgrvtx  47829  uhgrimisgrgric  47875  linccl  48307  ellcoellss  48328  elbigolo1  48454