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

Metamath Proof Explorer

Theorem axprlem3

Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023) (Proof shortened by Matthew House, 18-Sep-2025)

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 axrep4v 
 |-  ( 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 ) ) ) )
2 ifptru 
 |-  ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) )
3 2 biimpd 
 |-  ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) -> w = x ) )
4 equeuclr 
 |-  ( z = x -> ( w = x -> w = z ) )
5 3 4 syl9r 
 |-  ( z = x -> ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
6 5 alrimdv 
 |-  ( z = x -> ( E. n n e. s -> A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
7 6 spimevw 
 |-  ( E. n n e. s -> E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
8 ifpfal 
 |-  ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) )
9 8 biimpd 
 |-  ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) -> w = y ) )
10 equeuclr 
 |-  ( z = y -> ( w = y -> w = z ) )
11 9 10 syl9r 
 |-  ( z = y -> ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
12 11 alrimdv 
 |-  ( z = y -> ( -. E. n n e. s -> A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) ) )
13 12 spimevw 
 |-  ( -. E. n n e. s -> E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z ) )
14 7 13 pm2.61i 
 |-  E. z A. w ( if- ( E. n n e. s , w = x , w = y ) -> w = z )
15 1 14 mpg 
 |-  E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )