This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )