Theorem axprlem1

Description: Lemma for axpr . There exists a set to which all empty sets belong. (Contributed by Rohan Ridenour, 10-Aug-2023) (Revised by BJ, 13-Aug-2023) (Proof shortened by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	axprlem1	|- E. x A. y ( A. z -. z e. y -> y e. x )

Proof

Step	Hyp	Ref	Expression
1		ax-pow	|- E. x A. y ( A. z ( z e. y -> z e. w ) -> y e. x )
2		pm2.21	|- ( -. z e. y -> ( z e. y -> z e. w ) )
3	2	alimi	|- ( A. z -. z e. y -> A. z ( z e. y -> z e. w ) )
4	3	imim1i	|- ( ( A. z ( z e. y -> z e. w ) -> y e. x ) -> ( A. z -. z e. y -> y e. x ) )
5	4	alimi	|- ( A. y ( A. z ( z e. y -> z e. w ) -> y e. x ) -> A. y ( A. z -. z e. y -> y e. x ) )
6	1 5	eximii	|- E. x A. y ( A. z -. z e. y -> y e. x )