Theorem ssex 5261

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  ssexi  5262  ssexg  5263  intex  5284  moabexOLD  5410  naddunif  8626  ixpiunwdom  9502  omex  9561  tcss  9660  bndrank  9762  scottex  9806  aceq3lem  10039  cfslb  10185  dcomex  10366  axdc2lem  10367  grothpw  10746  grothpwex  10747  grothomex  10749  elnp  10907  negfi  12102  limsuple  15437  limsuplt  15438  limsupbnd1  15441  o1add2  15583  o1mul2  15584  o1sub2  15585  o1dif  15589  caucvgrlem  15632  fsumo1  15772  lcmfval  16587  lcmf0val  16588  unbenlem  16876  ressbas2  17205  prdsval  17415  prdsbas  17417  rescbas  17793  reschom  17794  rescco  17796  acsmapd  18517  issstrmgm  18618  issubmgm2  18668  issubmnd  18726  eqgfval  19148  dfod2  19536  ablfac1b  20044  islinds2  21809  pmatcollpw3lem  22764  2basgen  22971  prdstopn  23609  ressust  24244  rectbntr0  24814  elcncf  24872  cncfcnvcn  24908  cmssmscld  25333  cmsss  25334  ovolctb2  25475  limcfval  25855  ellimc2  25860  limcflf  25864  limcres  25869  limcun  25878  dvfval  25880  lhop2  25998  taylfval  26341  ulmval  26364  xrlimcnp  26951  axtgcont1  28556  ressnm  33045  ressprs  33047  ordtrestNEW  34087  ddeval1  34400  ddeval0  34401  carsgclctunlem3  34486  bnj849  35089  msrval  35742  mclsval  35767  brsset  36091  isfne4  36544  refssfne  36562  topjoin  36569  bj-snglex  37302  mblfinlem3  38002  filbcmb  38083  cnpwstotbnd  38140  ismtyval  38143  ispsubsp  40213  ispsubclN  40405  isnumbasgrplem2  43558  rtrclex  44070  brmptiunrelexpd  44136  iunrelexp0  44155  mulcncff  46324  subcncff  46334  addcncff  46338  cncfuni  46340  divcncff  46345  etransclem1  46689  etransclem4  46692  etransclem13  46701  isvonmbl  47092  isubgriedg  48359  isubgrvtx  48363  uhgrimisgrgric  48427  linccl  48910  ellcoellss  48931  elbigolo1  49053