Theorem rspw

Description: Restricted specialization. Weak version of rsp , requiring ax-8 , but not ax-12 . (Contributed by Gino Giotto, 3-Oct-2024)

	Ref	Expression
Hypothesis	rspw.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	rspw	|- ( A. x e. A ph -> ( x e. A -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		rspw.1	|- ( x = y -> ( ph <-> ps ) )
2		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
3		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
4	3 1	imbi12d	|- ( x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ps ) ) )
5	4	spw	|- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
6	2 5	sylbi	|- ( A. x e. A ph -> ( x e. A -> ph ) )