Theorem ssex 4835

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 4814 (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 3621	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 4833	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2718	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 223	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 207	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621

This theorem is referenced by:  ssexi  4836  ssexg  4837  intex  4850  moabex  4957  ixpiunwdom  8537  omex  8578  tcss  8658  bndrank  8742  scottex  8786  aceq3lem  8981  cfslb  9126  dcomex  9307  axdc2lem  9308  grothpw  9686  grothpwex  9687  grothomex  9689  elnp  9847  negfi  11009  hashfacen  13276  limsuple  14253  limsuplt  14254  limsupbnd1  14257  o1add2  14398  o1mul2  14399  o1sub2  14400  o1dif  14404  caucvgrlem  14447  fsumo1  14588  lcmfval  15381  lcmf0val  15382  unbenlem  15659  ressbas2  15978  prdsval  16162  prdsbas  16164  rescbas  16536  reschom  16537  rescco  16539  acsmapd  17225  issstrmgm  17299  issubmnd  17365  eqgfval  17689  dfod2  18027  ablfac1b  18515  islinds2  20200  pmatcollpw3lem  20636  2basgen  20842  prdstopn  21479  ressust  22115  rectbntr0  22682  elcncf  22739  cncfcnvcn  22771  cmsss  23193  ovolctb2  23306  limcfval  23681  ellimc2  23686  limcflf  23690  limcres  23695  limcun  23704  dvfval  23706  lhop2  23823  taylfval  24158  ulmval  24179  xrlimcnp  24740  axtgcont1  25412  fpwrelmap  29636  ressnm  29779  ressprs  29783  ordtrestNEW  30095  ddeval1  30425  ddeval0  30426  carsgclctunlem3  30510  bnj849  31121  msrval  31561  mclsval  31586  brsset  32121  isfne4  32460  refssfne  32478  topjoin  32485  bj-snglex  33086  mblfinlem3  33578  filbcmb  33665  cnpwstotbnd  33726  ismtyval  33729  ispsubsp  35349  ispsubclN  35541  isnumbasgrplem2  37991  rtrclex  38241  brmptiunrelexpd  38292  iunrelexp0  38311  mulcncff  40399  subcncff  40411  addcncff  40415  cncfuni  40417  divcncff  40422  etransclem1  40770  etransclem4  40773  etransclem13  40782  isvonmbl  41173  issubmgm2  42115  linccl  42528  ellcoellss  42549  elbigolo1  42676