Theorem ssex 5267

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 5242 (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 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5264	. . 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 3441   ∩ cin 3901   ⊆ wss 3902

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 5242

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 3401  df-v 3443  df-in 3909  df-ss 3919

This theorem is referenced by:  ssexi  5268  ssexg  5269  intex  5290  moabexOLD  5408  naddunif  8623  ixpiunwdom  9499  omex  9556  tcss  9655  bndrank  9757  scottex  9801  aceq3lem  10034  cfslb  10180  dcomex  10361  axdc2lem  10362  grothpw  10741  grothpwex  10742  grothomex  10744  elnp  10902  negfi  12095  limsuple  15405  limsuplt  15406  limsupbnd1  15409  o1add2  15551  o1mul2  15552  o1sub2  15553  o1dif  15557  caucvgrlem  15600  fsumo1  15739  lcmfval  16552  lcmf0val  16553  unbenlem  16840  ressbas2  17169  prdsval  17379  prdsbas  17381  rescbas  17757  reschom  17758  rescco  17760  acsmapd  18481  issstrmgm  18582  issubmgm2  18632  issubmnd  18690  eqgfval  19109  dfod2  19497  ablfac1b  20005  islinds2  21772  pmatcollpw3lem  22731  2basgen  22938  prdstopn  23576  ressust  24211  rectbntr0  24781  elcncf  24842  cncfcnvcn  24879  cmssmscld  25310  cmsss  25311  ovolctb2  25453  limcfval  25833  ellimc2  25838  limcflf  25842  limcres  25847  limcun  25856  dvfval  25858  lhop2  25980  taylfval  26326  ulmval  26349  xrlimcnp  26938  axtgcont1  28544  ressnm  33048  ressprs  33050  ordtrestNEW  34080  ddeval1  34393  ddeval0  34394  carsgclctunlem3  34479  bnj849  35083  msrval  35734  mclsval  35759  brsset  36083  isfne4  36536  refssfne  36554  topjoin  36561  bj-snglex  37176  mblfinlem3  37862  filbcmb  37943  cnpwstotbnd  38000  ismtyval  38003  ispsubsp  40073  ispsubclN  40265  isnumbasgrplem2  43413  rtrclex  43925  brmptiunrelexpd  43991  iunrelexp0  44010  mulcncff  46181  subcncff  46191  addcncff  46195  cncfuni  46197  divcncff  46202  etransclem1  46546  etransclem4  46549  etransclem13  46558  isvonmbl  46949  isubgriedg  48176  isubgrvtx  48180  uhgrimisgrgric  48244  linccl  48727  ellcoellss  48748  elbigolo1  48870