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

Metamath Proof Explorer

Theorem vtoclgf

Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003) (Proof shortened by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypotheses	vtoclgf.1	$⊢ \underline{Ⅎ} x A$
	vtoclgf.2	$⊢ Ⅎ x ψ$
	vtoclgf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
	vtoclgf.4	$⊢ φ$
Assertion	vtoclgf	$⊢ A \in V \to ψ$

Proof

Step	Hyp	Ref	Expression
1		vtoclgf.1	$⊢ \underline{Ⅎ} x A$
2		vtoclgf.2	$⊢ Ⅎ x ψ$
3		vtoclgf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
4		vtoclgf.4	$⊢ φ$
5		elex	$⊢ A \in V \to A \in V$
6	1	issetf	$⊢ A \in V \leftrightarrow \exists x x = A$
7	4 3	mpbii	$⊢ x = A \to ψ$
8	2 7	exlimi	$⊢ \exists x x = A \to ψ$
9	6 8	sylbi	$⊢ A \in V \to ψ$
10	5 9	syl	$⊢ A \in V \to ψ$