Theorem el 3485

Description: Every set is an element of some other set. See elALT 3494 for a shorter proof using more axioms. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

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

Distinct variable group:   x,y

Proof of Theorem el

Step	Hyp	Ref	Expression
1		zfpow 3482	. 2 |- E.yA.z(A.y(y e. z -> y e. x) -> z e. y)
2		ax-14 1312	. . . . . 6 |- (z = x -> (y e. z -> y e. x))
3	2	19.21aiv 1664	. . . . 5 |- (z = x -> A.y(y e. z -> y e. x))
4		ax-13 1311	. . . . . 6 |- (z = x -> (z e. y -> x e. y))
5	4	imim2d 28	. . . . 5 |- (z = x -> ((A.y(y e. z -> y e. x) -> z e. y) -> (A.y(y e. z -> y e. x) -> x e. y)))
6		pm2.27 76	. . . . 5 |- (A.y(y e. z -> y e. x) -> ((A.y(y e. z -> y e. x) -> x e. y) -> x e. y))
7	3, 5, 6	sylsyld 32	. . . 4 |- (z = x -> ((A.y(y e. z -> y e. x) -> z e. y) -> x e. y))
8	7	a4imv 1576	. . 3 |- (A.z(A.y(y e. z -> y e. x) -> z e. y) -> x e. y)
9	8	eximi 1387	. 2 |- (E.yA.z(A.y(y e. z -> y e. x) -> z e. y) -> E.y x e. y)
10	1, 9	ax-mp 7	1 |- E.y x e. y

Syntax hints:   -> wi 3  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326

This theorem is referenced by:  dvdemo2 3521  axpownd 6105  zfcndinf 6122  domep 13861  distel 13870

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-pow 3481

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain