Theorem ssex 3654

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 3638 (a.k.a. Subset Axiom).

Hypothesis

Ref	Expression
ssex.1	|- B e. _V

Assertion

Ref	Expression
ssex	|- (A C_ B -> A e. _V)

Proof of Theorem ssex

Step	Hyp	Ref	Expression
1		df-ss 2868	. 2 |- (A C_ B <-> (A i^i B) = A)
2		ssex.1	. . . 4 |- B e. _V
3	2	inex2 3652	. . 3 |- (A i^i B) e. _V
4		eleq1 2233	. . 3 |- ((A i^i B) = A -> ((A i^i B) e. _V <-> A e. _V))
5	3, 4	mpbii 258	. 2 |- ((A i^i B) = A -> A e. _V)
6	1, 5	sylbi 237	1 |- (A C_ B -> A e. _V)

Syntax hints:   -> wi 3   = wceq 1615   e. wcel 1617  _Vcvv 2569   i^i cin 2858   C_ wss 2859

This theorem is referenced by:  ssexi 3655  ssexg 3656  intex 3664  elpm 5599  mapss 5609  ordtypelem4 5962  inf3lem7OLD 6002  omex 6010  unbnn3 6026  bndrank 6094  scottex 6150  dcomex 6373  zorn2lem4 6438  ondomon 6497  elnp 6687  suplem2pr 6757  lbinfm 7705  supcvg 8993  supcvgOLD 8995  elcncf 9043  unbenlem 9522  lpval 10035  lmclim 10257  vacnlem4 10691  grothpw 11161  grothpwex 11162  grothomex 11164  sh 11705  bnj879 13735  bnj880 13736  brsset 15001  supnuf 16096  supexr 16098  ordtypelem4OLD 16463  filclus 16690  filbcmb 16861  heiborlem1 17040  igenval 17294  iscsubsp 18189  ispsubsp 18450  ispsubcl 18623

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-v 2571  df-in 2866  df-ss 2868

Copyright terms: Public domain