Theorem ssex 4802

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ∩ cin 3573   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  ssexi  4803  ssexg  4804  intex  4820  moabex  4927  ixpiunwdom  8496  omex  8540  tcss  8620  bndrank  8704  scottex  8748  aceq3lem  8943  cfslb  9088  dcomex  9269  axdc2lem  9270  grothpw  9648  grothpwex  9649  grothomex  9651  elnp  9809  negfi  10971  hashfacen  13238  limsuple  14209  limsuplt  14210  limsupbnd1  14213  o1add2  14354  o1mul2  14355  o1sub2  14356  o1dif  14360  caucvgrlem  14403  fsumo1  14544  lcmfval  15334  lcmf0val  15335  unbenlem  15612  ressbas2  15931  prdsval  16115  prdsbas  16117  rescbas  16489  reschom  16490  rescco  16492  acsmapd  17178  issstrmgm  17252  issubmnd  17318  eqgfval  17642  dfod2  17981  ablfac1b  18469  islinds2  20152  pmatcollpw3lem  20588  2basgen  20794  prdstopn  21431  ressust  22068  rectbntr0  22635  elcncf  22692  cncfcnvcn  22724  cmsss  23147  ovolctb2  23260  limcfval  23636  ellimc2  23641  limcflf  23645  limcres  23650  limcun  23659  dvfval  23661  lhop2  23778  taylfval  24113  ulmval  24134  xrlimcnp  24695  axtgcont1  25367  fpwrelmap  29508  ressnm  29651  ressprs  29655  ordtrestNEW  29967  ddeval1  30297  ddeval0  30298  carsgclctunlem3  30382  bnj849  30995  msrval  31435  mclsval  31460  brsset  31996  isfne4  32335  refssfne  32353  topjoin  32360  bj-snglex  32961  mblfinlem3  33448  filbcmb  33535  cnpwstotbnd  33596  ismtyval  33599  ispsubsp  35031  ispsubclN  35223  isnumbasgrplem2  37674  rtrclex  37924  brmptiunrelexpd  37975  iunrelexp0  37994  mulcncff  40081  subcncff  40093  addcncff  40097  cncfuni  40099  divcncff  40104  etransclem1  40452  etransclem4  40455  etransclem13  40464  isvonmbl  40852  issubmgm2  41790  linccl  42203  ellcoellss  42224  elbigolo1  42351