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)

	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	a1i	|- ( A. z -. z e. w -> ( A. z -. z e. y -> A. z ( z e. y -> z e. w ) ) )
5	4	imim1d	|- ( A. z -. z e. w -> ( ( A. z ( z e. y -> z e. w ) -> y e. x ) -> ( A. z -. z e. y -> y e. x ) ) )
6	5	alimdv	|- ( A. z -. z e. w -> ( A. y ( A. z ( z e. y -> z e. w ) -> y e. x ) -> A. y ( A. z -. z e. y -> y e. x ) ) )
7	6	eximdv	|- ( A. z -. z e. w -> ( E. x A. y ( A. z ( z e. y -> z e. w ) -> y e. x ) -> E. x A. y ( A. z -. z e. y -> y e. x ) ) )
8	1 7	mpi	|- ( A. z -. z e. w -> E. x A. y ( A. z -. z e. y -> y e. x ) )
9		ax-nul	|- E. w A. z -. z e. w
10	8 9	exlimiiv	|- E. x A. y ( A. z -. z e. y -> y e. x )