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\to \left(\phi \leftrightarrow \psi \right)$$
	vtoclri.2	$$⊢\forall x\in B\phi$$
Assertion	vtoclri	$$⊢A\in B\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		vtoclri.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		vtoclri.2	$$⊢\forall x\in B\phi$$
3	2	rspec	$$⊢x\in B\to \phi$$
4	1 3	vtoclga	$$⊢A\in B\to \psi$$