Theorem ssex 5228

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 5206 (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 3955	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5225	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2903	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 235	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 219	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  Vcvv 3497   ∩ cin 3938   ⊆ wss 3939

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-in 3946  df-ss 3955

This theorem is referenced by:  ssexi  5229  ssexg  5230  intex  5243  moabex  5354  ixpiunwdom  9058  omex  9109  tcss  9189  bndrank  9273  scottex  9317  aceq3lem  9549  cfslb  9691  dcomex  9872  axdc2lem  9873  grothpw  10251  grothpwex  10252  grothomex  10254  elnp  10412  negfi  11592  hashfacen  13815  limsuple  14838  limsuplt  14839  limsupbnd1  14842  o1add2  14983  o1mul2  14984  o1sub2  14985  o1dif  14989  caucvgrlem  15032  fsumo1  15170  lcmfval  15968  lcmf0val  15969  unbenlem  16247  ressbas2  16558  prdsval  16731  prdsbas  16733  rescbas  17102  reschom  17103  rescco  17105  acsmapd  17791  issstrmgm  17866  issubmnd  17941  eqgfval  18331  dfod2  18694  ablfac1b  19195  islinds2  20960  pmatcollpw3lem  21394  2basgen  21601  prdstopn  22239  ressust  22876  rectbntr0  23443  elcncf  23500  cncfcnvcn  23532  cmssmscld  23956  cmsss  23957  ovolctb2  24096  limcfval  24473  ellimc2  24478  limcflf  24482  limcres  24487  limcun  24496  dvfval  24498  lhop2  24615  taylfval  24950  ulmval  24971  xrlimcnp  25549  axtgcont1  26257  fpwrelmap  30472  ressnm  30642  ressprs  30646  ordtrestNEW  31168  ddeval1  31497  ddeval0  31498  carsgclctunlem3  31582  bnj849  32201  msrval  32789  mclsval  32814  brsset  33354  isfne4  33692  refssfne  33710  topjoin  33717  bj-snglex  34289  mblfinlem3  34935  filbcmb  35019  cnpwstotbnd  35079  ismtyval  35082  ispsubsp  36885  ispsubclN  37077  isnumbasgrplem2  39710  rtrclex  39983  brmptiunrelexpd  40034  iunrelexp0  40053  mulcncff  42157  subcncff  42169  addcncff  42173  cncfuni  42175  divcncff  42180  etransclem1  42527  etransclem4  42530  etransclem13  42539  isvonmbl  42927  issubmgm2  44064  linccl  44476  ellcoellss  44497  elbigolo1  44624