Theorem bnj1464

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1464.1	|- ( ps -> A. x ps )
	bnj1464.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	bnj1464	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1464.1	|- ( ps -> A. x ps )
2		bnj1464.2	|- ( x = A -> ( ph <-> ps ) )
3	1	nf5i	|- F/ x ps
4	3 2	sbciegf	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )