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	$$⊢\exists yx\in y$$

Proof

Step	Hyp	Ref	Expression
1		zfpow	$$⊢\exists y\forall z\left(\forall y\left(y\in z\to y\in x\right)\to z\in y\right)$$
2		ax9	$$⊢z=x\to \left(y\in z\to y\in x\right)$$
3	2	alrimiv	$$⊢z=x\to \forall y\left(y\in z\to y\in x\right)$$
4		ax8	$$⊢z=x\to \left(z\in y\to x\in y\right)$$
5	3 4	embantd	$$⊢z=x\to \left(\left(\forall y\left(y\in z\to y\in x\right)\to z\in y\right)\to x\in y\right)$$
6	5	spimvw	$$⊢\forall z\left(\forall y\left(y\in z\to y\in x\right)\to z\in y\right)\to x\in y$$
7	1 6	eximii	$$⊢\exists yx\in y$$