Theorem vtoclri

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994)

	Ref	Expression
Hypotheses	vtoclri.1	|- ( x = A -> ( ph <-> ps ) )
	vtoclri.2	|- A. x e. B ph
Assertion	vtoclri	|- ( A e. B -> ps )

Proof

Step	Hyp	Ref	Expression
1		vtoclri.1	|- ( x = A -> ( ph <-> ps ) )
2		vtoclri.2	|- A. x e. B ph
3	2	rspec	|- ( x e. B -> ph )
4	1 3	vtoclga	|- ( A e. B -> ps )