# Metamath Proof Explorer

## 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 {y}\phantom{\rule{.4em}{0ex}}{x}\in {y}$

### Proof

Step Hyp Ref Expression
1 zfpow ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\to {y}\in {x}\right)\to {z}\in {y}\right)\to {x}\in {y}\right)$
6 5 spimvw ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}\to {y}\in {x}\right)\to {z}\in {y}\right)\to {x}\in {y}$
7 1 6 eximii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{x}\in {y}$