Theorem ssex 2719

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

Hypothesis

Ref	Expression
ssex.1	|- B e. V

Assertion

Ref	Expression
ssex	|- (A (_ B -> A e. V)

Proof of Theorem ssex

Step	Hyp	Ref	Expression
1		df-ss 2053	. 2 |- (A (_ B <-> (A i^i B) = A)
2		ssex.1	. . . 4 |- B e. V
3	2	inex2 2717	. . 3 |- (A i^i B) e. V
4		eleq1 1534	. . 3 |- ((A i^i B) = A -> ((A i^i B) e. V <-> A e. V))
5	3, 4	mpbii 193	. 2 |- ((A i^i B) = A -> A e. V)
6	1, 5	sylbi 199	1 |- (A (_ B -> A e. V)

Syntax hints:   -> wi 3   = wceq 956   e. wcel 958  Vcvv 1811   i^i cin 2046   (_ wss 2047

This theorem is referenced by:  ssexi 2720  ssexg 2721  intex 2729  elpm 4336  mapss 4346  inf3lem7 4619  omex 4627  unbnnt 4639  bndrank 4682  scottex 4716  zorn2lem4 4791  ondomon 4856  elnp 5092  suplem2pr 5162  lbinfm 6048  elcncf 7265  unbenlem 7504  lpval 7743  lmclim 7963  sh 9078

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053

Copyright terms: Public domain