Theorem el

Description: Every set is an element of some other set. See elALT for a shorter proof using more axioms. (Contributed by NM, 4-Jan-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	el	|- E. y x e. y

Proof

Step	Hyp	Ref	Expression
1		zfpow	|- E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y )
2		ax9	|- ( z = x -> ( y e. z -> y e. x ) )
3	2	alrimiv	|- ( z = x -> A. y ( y e. z -> y e. x ) )
4		ax8	|- ( z = x -> ( z e. y -> x e. y ) )
5	3 4	embantd	|- ( z = x -> ( ( A. y ( y e. z -> y e. x ) -> z e. y ) -> x e. y ) )
6	5	spimvw	|- ( A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) -> x e. y )
7	1 6	eximii	|- E. y x e. y