Theorem equs5av

Description: A property related to substitution that replaces the distinctor from equs5 to a disjoint variable condition. Version of equs5a with a disjoint variable condition, which does not require ax-13 . See also sbalex . (Contributed by NM, 2-Feb-2007) (Revised by Gino Giotto, 15-Dec-2023)

	Ref	Expression
Assertion	equs5av	|- ( E. x ( x = y /\ A. y ph ) -> A. x ( x = y -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfa1	|- F/ x A. x ( x = y -> ph )
2		ax12v2	|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
3	2	spsd	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
4	3	imp	|- ( ( x = y /\ A. y ph ) -> A. x ( x = y -> ph ) )
5	1 4	exlimi	|- ( E. x ( x = y /\ A. y ph ) -> A. x ( x = y -> ph ) )