Theorem vtocl2

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Hypotheses	vtocl2.1	|- A e. _V
	vtocl2.2	|- B e. _V
	vtocl2.3	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
	vtocl2.4	|- ph
Assertion	vtocl2	|- ps

Proof

Step	Hyp	Ref	Expression
1		vtocl2.1	|- A e. _V
2		vtocl2.2	|- B e. _V
3		vtocl2.3	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
4		vtocl2.4	|- ph
5	4	a1i	|- ( y = B -> ph )
6	3	pm5.74da	|- ( x = A -> ( ( y = B -> ph ) <-> ( y = B -> ps ) ) )
7	1 6 5	vtocl	|- ( y = B -> ps )
8	5 7	2thd	|- ( y = B -> ( ph <-> ps ) )
9	2 8 4	vtocl	|- ps