Metamath Proof Explorer

Theorem wl-ax11-lem5

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

		Ref	Expression
	Assertion	wl-ax11-lem5	\|- ( A. u u = y -> ( A. u [ u / y ] ph <-> A. y ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ12r	\|- ( u = y -> ( [ u / y ] ph <-> ph ) )
2	1	sps	\|- ( A. u u = y -> ( [ u / y ] ph <-> ph ) )
3	2	dral1	\|- ( A. u u = y -> ( A. u [ u / y ] ph <-> A. y ph ) )