Theorem ssex 2687

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 2671 (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 2024	. 2 |- (A (_ B <-> (A i^i B) = A)
2		ssex.1	. . . 4 |- B e. V
3	2	inex2 2685	. . 3 |- (A i^i B) e. V
4		eleq1 1510	. . 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 1099   e. wcel 1105  Vcvv 1786   i^i cin 2017   (_ wss 2018

This theorem is referenced by:  ssexi 2688  ssexg 2689  intex 2697  elpm 4274  mapss 4284  inf3lem7 4543  omex 4551  unbnnt 4563  bndrank 4606  scottex 4640  zorn2lem4 4715  ondomon 4779  elnp 5015  suplem2pr 5085  lbinfm 5946  elcncf 7151  unbenlem 7398  lpval 7632  lmclim 7846  sh 9229

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-in 2022  df-ss 2024

Copyright terms: Public domain