Metamath Proof Explorer

Theorem axprlem3

Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023)

Ref Expression
Assertion axprlem3 
|- E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ z if- ( E. n n e. s , w = x , w = y )
2 1 axrep4 
 |-  ( A. s E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) -> E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
3 ax6evr 
 |-  E. z x = z
4 ifptru 
 |-  ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) )
5 4 biimpd 
 |-  ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) -> w = x ) )
6 equtrr 
 |-  ( x = z -> ( w = x -> w = z ) )
7 5 6 sylan9r 
 |-  ( ( x = z /\ E. n n e. s ) -> ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
8 7 alrimiv 
 |-  ( ( x = z /\ E. n n e. s ) -> A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
9 8 expcom 
 |-  ( E. n n e. s -> ( x = z -> A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
10 9 eximdv 
 |-  ( E. n n e. s -> ( E. z x = z -> E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
11 3 10 mpi 
 |-  ( E. n n e. s -> E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
12 ax6evr 
 |-  E. z y = z
13 ifpfal 
 |-  ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) )
14 13 biimpd 
 |-  ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) -> w = y ) )
15 14 adantl 
 |-  ( ( y = z /\ -. E. n n e. s ) -> ( if- ( E. n n e. s , w = x , w = y ) -> w = y ) )
16 simpl 
 |-  ( ( y = z /\ -. E. n n e. s ) -> y = z )
17 equtr 
 |-  ( w = y -> ( y = z -> w = z ) )
18 15 16 17 syl6ci 
 |-  ( ( y = z /\ -. E. n n e. s ) -> ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
19 18 alrimiv 
 |-  ( ( y = z /\ -. E. n n e. s ) -> A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
20 19 expcom 
 |-  ( -. E. n n e. s -> ( y = z -> A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
21 20 eximdv 
 |-  ( -. E. n n e. s -> ( E. z y = z -> E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
22 12 21 mpi 
 |-  ( -. E. n n e. s -> E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
23 11 22 pm2.61i 
 |-  E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z )
24 2 23 mpg 
 |-  E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )