Theorem ssex 5276

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ∩ cin 3913   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  ssexi  5277  ssexg  5278  intex  5299  moabex  5419  naddunif  8657  ixpiunwdom  9543  omex  9596  tcss  9697  bndrank  9794  scottex  9838  aceq3lem  10073  cfslb  10219  dcomex  10400  axdc2lem  10401  grothpw  10779  grothpwex  10780  grothomex  10782  elnp  10940  negfi  12132  limsuple  15444  limsuplt  15445  limsupbnd1  15448  o1add2  15590  o1mul2  15591  o1sub2  15592  o1dif  15596  caucvgrlem  15639  fsumo1  15778  lcmfval  16591  lcmf0val  16592  unbenlem  16879  ressbas2  17208  prdsval  17418  prdsbas  17420  rescbas  17791  reschom  17792  rescco  17794  acsmapd  18513  issstrmgm  18580  issubmgm2  18630  issubmnd  18688  eqgfval  19108  dfod2  19494  ablfac1b  20002  islinds2  21722  pmatcollpw3lem  22670  2basgen  22877  prdstopn  23515  ressust  24151  rectbntr0  24721  elcncf  24782  cncfcnvcn  24819  cmssmscld  25250  cmsss  25251  ovolctb2  25393  limcfval  25773  ellimc2  25778  limcflf  25782  limcres  25787  limcun  25796  dvfval  25798  lhop2  25920  taylfval  26266  ulmval  26289  xrlimcnp  26878  axtgcont1  28395  fpwrelmap  32656  ressnm  32886  ressprs  32890  ordtrestNEW  33911  ddeval1  34224  ddeval0  34225  carsgclctunlem3  34311  bnj849  34915  msrval  35525  mclsval  35550  brsset  35877  isfne4  36328  refssfne  36346  topjoin  36353  bj-snglex  36961  mblfinlem3  37653  filbcmb  37734  cnpwstotbnd  37791  ismtyval  37794  ispsubsp  39739  ispsubclN  39931  isnumbasgrplem2  43093  rtrclex  43606  brmptiunrelexpd  43672  iunrelexp0  43691  mulcncff  45868  subcncff  45878  addcncff  45882  cncfuni  45884  divcncff  45889  etransclem1  46233  etransclem4  46236  etransclem13  46245  isvonmbl  46636  isubgriedg  47863  isubgrvtx  47867  uhgrimisgrgric  47931  linccl  48403  ellcoellss  48424  elbigolo1  48546