Theorem ssex 5078

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 5057 (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 3838	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5076	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2848	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 225	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 209	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  Vcvv 3410   ∩ cin 3823   ⊆ wss 3824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745  ax-sep 5057

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-in 3831  df-ss 3838

This theorem is referenced by:  ssexi  5079  ssexg  5080  intex  5093  moabex  5205  ixpiunwdom  8849  omex  8899  tcss  8979  bndrank  9063  scottex  9107  aceq3lem  9339  cfslb  9485  dcomex  9666  axdc2lem  9667  grothpw  10045  grothpwex  10046  grothomex  10048  elnp  10206  negfi  11389  hashfacen  13624  limsuple  14695  limsuplt  14696  limsupbnd1  14699  o1add2  14840  o1mul2  14841  o1sub2  14842  o1dif  14846  caucvgrlem  14889  fsumo1  15026  lcmfval  15820  lcmf0val  15821  unbenlem  16099  ressbas2  16410  prdsval  16583  prdsbas  16585  rescbas  16970  reschom  16971  rescco  16973  acsmapd  17659  issstrmgm  17733  issubmnd  17799  eqgfval  18124  dfod2  18465  ablfac1b  18955  islinds2  20675  pmatcollpw3lem  21111  2basgen  21318  prdstopn  21956  ressust  22592  rectbntr0  23159  elcncf  23216  cncfcnvcn  23248  cmssmscld  23672  cmsss  23673  ovolctb2  23812  limcfval  24189  ellimc2  24194  limcflf  24198  limcres  24203  limcun  24212  dvfval  24214  lhop2  24331  taylfval  24666  ulmval  24687  xrlimcnp  25264  axtgcont1  25972  fpwrelmap  30246  ressnm  30397  ressprs  30401  ordtrestNEW  30841  ddeval1  31171  ddeval0  31172  carsgclctunlem3  31256  bnj849  31877  msrval  32338  mclsval  32363  brsset  32904  isfne4  33242  refssfne  33260  topjoin  33267  bj-snglex  33836  mblfinlem3  34405  filbcmb  34490  cnpwstotbnd  34550  ismtyval  34553  ispsubsp  36359  ispsubclN  36551  isnumbasgrplem2  39134  rtrclex  39374  brmptiunrelexpd  39425  iunrelexp0  39444  mulcncff  41611  subcncff  41623  addcncff  41627  cncfuni  41629  divcncff  41634  etransclem1  41981  etransclem4  41984  etransclem13  41993  isvonmbl  42381  issubmgm2  43455  linccl  43866  ellcoellss  43887  elbigolo1  44015