This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V$
	vtocl2.2	$⊢ B \in V$
	vtocl2.3	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
	vtocl2.4	$⊢ φ$
Assertion	vtocl2	$⊢ ψ$

Proof

Step	Hyp	Ref	Expression
1		vtocl2.1	$⊢ A \in V$
2		vtocl2.2	$⊢ B \in V$
3		vtocl2.3	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
4		vtocl2.4	$⊢ φ$
5	4	a1i	$⊢ y = B \to φ$
6	3	pm5.74da	$⊢ x = A \to ((y = B \to φ) \leftrightarrow (y = B \to ψ))$
7	1 6 5	vtocl	$⊢ y = B \to ψ$
8	5 7	2thd	$⊢ y = B \to (φ \leftrightarrow ψ)$
9	2 8 4	vtocl	$⊢ ψ$