Theorem bj-equsal1ti

Description: Inference associated with bj-equsal1t . (Contributed by BJ, 30-Sep-2018)

	Ref	Expression
Hypothesis	bj-equsal1ti.1	|- F/ x ph
Assertion	bj-equsal1ti	|- ( A. x ( x = y -> ph ) <-> ph )

Proof

Step	Hyp	Ref	Expression
1		bj-equsal1ti.1	|- F/ x ph
2		bj-equsal1t	|- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) )
3	1 2	ax-mp	|- ( A. x ( x = y -> ph ) <-> ph )