Theorem axprlem2

Description: Lemma for axpr . There exists a set to which all sets whose only members are empty sets belong. (Contributed by Rohan Ridenour, 9-Aug-2023) (Revised by BJ, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		ax-pow	|- E. x A. y ( A. z ( z e. y -> z e. v ) -> y e. x )
2		df-ral	|- ( A. z e. y A. w -. w e. z <-> A. z ( z e. y -> A. w -. w e. z ) )
3		imim2	|- ( ( A. w -. w e. z -> z e. v ) -> ( ( z e. y -> A. w -. w e. z ) -> ( z e. y -> z e. v ) ) )
4	3	al2imi	|- ( A. z ( A. w -. w e. z -> z e. v ) -> ( A. z ( z e. y -> A. w -. w e. z ) -> A. z ( z e. y -> z e. v ) ) )
5	2 4	biimtrid	|- ( A. z ( A. w -. w e. z -> z e. v ) -> ( A. z e. y A. w -. w e. z -> A. z ( z e. y -> z e. v ) ) )
6	5	imim1d	|- ( A. z ( A. w -. w e. z -> z e. v ) -> ( ( A. z ( z e. y -> z e. v ) -> y e. x ) -> ( A. z e. y A. w -. w e. z -> y e. x ) ) )
7	6	alimdv	|- ( A. z ( A. w -. w e. z -> z e. v ) -> ( A. y ( A. z ( z e. y -> z e. v ) -> y e. x ) -> A. y ( A. z e. y A. w -. w e. z -> y e. x ) ) )
8	7	eximdv	|- ( A. z ( A. w -. w e. z -> z e. v ) -> ( E. x A. y ( A. z ( z e. y -> z e. v ) -> y e. x ) -> E. x A. y ( A. z e. y A. w -. w e. z -> y e. x ) ) )
9	1 8	mpi	|- ( A. z ( A. w -. w e. z -> z e. v ) -> E. x A. y ( A. z e. y A. w -. w e. z -> y e. x ) )
10		axprlem1	|- E. v A. z ( A. w -. w e. z -> z e. v )
11	9 10	exlimiiv	|- E. x A. y ( A. z e. y A. w -. w e. z -> y e. x )