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

Metamath Proof Explorer

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