Theorem ssex 2793

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 2777 (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 2105	. 2 |- (A (_ B <-> (A i^i B) = A)
2		ssex.1	. . . 4 |- B e. V
3	2	inex2 2791	. . 3 |- (A i^i B) e. V
4		eleq1 1577	. . 3 |- ((A i^i B) = A -> ((A i^i B) e. V <-> A e. V))
5	3, 4	mpbii 191	. 2 |- ((A i^i B) = A -> A e. V)
6	1, 5	sylbi 197	1 |- (A (_ B -> A e. V)

Syntax hints:   -> wi 3   = wceq 992   e. wcel 994  Vcvv 1857   i^i cin 2098   (_ wss 2099

This theorem is referenced by:  ssexi 2794  ssexg 2795  intex 2803  elpm 4477  mapss 4487  inf3lem7 4764  omex 4772  unbnn3 4785  bndrank 4828  scottex 4862  zorn2lem4 4937  ondomon 5006  elnp 5246  suplem2pr 5316  lbinfm 6216  elcncf 7470  unbenlem 7716  lpval 7953  lmclim 8174  vacnlem4 8585  grothpw 9054  sh 9354  ordtypelem4 11430  filclus 11717  filbcmb 11857  heiborlem1 12011

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105

Copyright terms: Public domain