Theorem ssex 5245

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 5223 (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 3904	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5242	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2826	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 232	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 216	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  ssexi  5246  ssexg  5247  intex  5261  moabex  5374  ixpiunwdom  9349  omex  9401  tcss  9502  bndrank  9599  scottex  9643  aceq3lem  9876  cfslb  10022  dcomex  10203  axdc2lem  10204  grothpw  10582  grothpwex  10583  grothomex  10585  elnp  10743  negfi  11924  hashfacenOLD  14167  limsuple  15187  limsuplt  15188  limsupbnd1  15191  o1add2  15333  o1mul2  15334  o1sub2  15335  o1dif  15339  caucvgrlem  15384  fsumo1  15524  lcmfval  16326  lcmf0val  16327  unbenlem  16609  ressbas2  16949  prdsval  17166  prdsbas  17168  rescbas  17541  rescbasOLD  17542  reschom  17543  rescco  17545  resccoOLD  17546  acsmapd  18272  issstrmgm  18337  issubmnd  18412  eqgfval  18804  dfod2  19171  ablfac1b  19673  islinds2  21020  pmatcollpw3lem  21932  2basgen  22140  prdstopn  22779  ressust  23415  rectbntr0  23995  elcncf  24052  cncfcnvcn  24088  cmssmscld  24514  cmsss  24515  ovolctb2  24656  limcfval  25036  ellimc2  25041  limcflf  25045  limcres  25050  limcun  25059  dvfval  25061  lhop2  25179  taylfval  25518  ulmval  25539  xrlimcnp  26118  axtgcont1  26829  fpwrelmap  31068  ressnm  31236  ressprs  31241  ordtrestNEW  31871  ddeval1  32202  ddeval0  32203  carsgclctunlem3  32287  bnj849  32905  msrval  33500  mclsval  33525  brsset  34191  isfne4  34529  refssfne  34547  topjoin  34554  bj-snglex  35163  mblfinlem3  35816  filbcmb  35898  cnpwstotbnd  35955  ismtyval  35958  ispsubsp  37759  ispsubclN  37951  isnumbasgrplem2  40929  rtrclex  41225  brmptiunrelexpd  41291  iunrelexp0  41310  mulcncff  43411  subcncff  43421  addcncff  43425  cncfuni  43427  divcncff  43432  etransclem1  43776  etransclem4  43779  etransclem13  43788  isvonmbl  44176  issubmgm2  45344  linccl  45755  ellcoellss  45776  elbigolo1  45903