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 ) ) )