Theorem ssex 4963

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 4941 (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 3746	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 4961	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2832	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 224	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 208	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1652   ∈ wcel 2155  Vcvv 3350   ∩ cin 3731   ⊆ wss 3732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743  ax-sep 4941

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3739  df-ss 3746

This theorem is referenced by:  ssexi  4964  ssexg  4965  intex  4978  moabex  5083  ixpiunwdom  8703  omex  8755  tcss  8835  bndrank  8919  scottex  8963  aceq3lem  9194  cfslb  9341  dcomex  9522  axdc2lem  9523  grothpw  9901  grothpwex  9902  grothomex  9904  elnp  10062  negfi  11225  hashfacen  13439  limsuple  14494  limsuplt  14495  limsupbnd1  14498  o1add2  14639  o1mul2  14640  o1sub2  14641  o1dif  14645  caucvgrlem  14688  fsumo1  14828  lcmfval  15615  lcmf0val  15616  unbenlem  15891  ressbas2  16203  prdsval  16381  prdsbas  16383  rescbas  16754  reschom  16755  rescco  16757  acsmapd  17444  issstrmgm  17518  issubmnd  17584  eqgfval  17906  dfod2  18245  ablfac1b  18736  islinds2  20428  pmatcollpw3lem  20867  2basgen  21074  prdstopn  21711  ressust  22347  rectbntr0  22914  elcncf  22971  cncfcnvcn  23003  cmssmscld  23427  cmsss  23428  ovolctb2  23550  limcfval  23927  ellimc2  23932  limcflf  23936  limcres  23941  limcun  23950  dvfval  23952  lhop2  24069  taylfval  24404  ulmval  24425  xrlimcnp  24986  axtgcont1  25658  fpwrelmap  29957  ressnm  30098  ressprs  30102  ordtrestNEW  30414  ddeval1  30744  ddeval0  30745  carsgclctunlem3  30829  bnj849  31443  msrval  31883  mclsval  31908  brsset  32440  isfne4  32778  refssfne  32796  topjoin  32803  bj-snglex  33388  mblfinlem3  33872  filbcmb  33958  cnpwstotbnd  34018  ismtyval  34021  ispsubsp  35701  ispsubclN  35893  isnumbasgrplem2  38351  rtrclex  38599  brmptiunrelexpd  38650  iunrelexp0  38669  mulcncff  40719  subcncff  40731  addcncff  40735  cncfuni  40737  divcncff  40742  etransclem1  41089  etransclem4  41092  etransclem13  41101  isvonmbl  41492  issubmgm2  42459  linccl  42872  ellcoellss  42893  elbigolo1  43020