Theorem ssex 5292

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 5259 (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 3929	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5289	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2857	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 236	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3461   ∩ cin 3910   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-in 3918  df-ss 3928

This theorem is referenced by:  ssexi  5293  ssexg  5294  intex  5315  moabexOLD  5441  naddunif  8680  ixpiunwdom  9552  omex  9612  tcss  9711  bndrank  9813  scottex  9859  aceq3lem  10104  cfslb  10250  dcomex  10431  axdc2lem  10432  grothpw  10811  grothpwex  10812  grothomex  10814  elnp  10972  negfi  12164  limsuple  15529  limsuplt  15530  limsupbnd1  15533  o1add2  15675  o1mul2  15676  o1sub2  15677  o1dif  15681  caucvgrlem  15724  fsumo1  15864  lcmfval  16679  lcmf0val  16680  unbenlem  16968  ressbas2  17298  prdsval  17508  prdsbas  17510  rescbas  17886  reschom  17887  rescco  17889  acsmapd  18610  issstrmgm  18711  issubmgm2  18761  issubmnd  18819  eqgfval  19244  dfod2  19634  ablfac1b  20142  islinds2  21932  pmatcollpw3lem  22909  2basgen  23116  prdstopn  23754  ressust  24389  rectbntr0  24959  elcncf  25017  cncfcnvcn  25053  cmssmscld  25478  cmsss  25479  ovolctb2  25620  limcfval  26000  ellimc2  26005  limcflf  26009  limcres  26014  limcun  26023  dvfval  26025  lhop2  26143  taylfval  26488  ulmval  26509  xrlimcnp  27099  axtgcont1  28703  ressnm  33225  ressprs  33227  ordtrestNEW  34256  ddeval1  34569  ddeval0  34570  carsgclctunlem3  34655  bnj849  35258  msrval  35963  mclsval  35988  brsset  36312  isfne4  36774  refssfne  36792  topjoin  36799  bj-snglex  37532  mblfinlem3  38233  filbcmb  38314  cnpwstotbnd  38371  ismtyval  38374  ispsubsp  40444  ispsubclN  40636  isnumbasgrplem2  43758  rtrclex  44270  brmptiunrelexpd  44336  iunrelexp0  44355  mulcncff  46511  subcncff  46521  addcncff  46525  cncfuni  46527  divcncff  46532  etransclem1  46876  etransclem4  46879  etransclem13  46888  isvonmbl  47279  isubgriedg  48552  isubgrvtx  48556  uhgrimisgrgric  48620  linccl  49114  ellcoellss  49135  elbigolo1  49257