Theorem ssex 2714

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 2698 (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 2049	. 2 |- (A (_ B <-> (A i^i B) = A)
2		ssex.1	. . . 4 |- B e. V
3	2	inex2 2712	. . 3 |- (A i^i B) e. V
4		eleq1 1531	. . 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 954   e. wcel 956  Vcvv 1807   i^i cin 2042   (_ wss 2043

This theorem is referenced by:  ssexi 2715  ssexg 2716  intex 2724  elpm 4326  mapss 4336  inf3lem7 4599  omex 4607  unbnnt 4619  bndrank 4662  scottex 4696  zorn2lem4 4771  ondomon 4836  elnp 5072  suplem2pr 5142  lbinfm 6003  elcncf 7208  unbenlem 7455  lpval 7693  lmclim 7914  sh 9017

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain