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	$$⊢\underset{\_}{Ⅎ}xA$$
	vtoclgf.2	$$⊢Ⅎx\psi$$
	vtoclgf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	vtoclgf.4	$$⊢\phi$$
Assertion	vtoclgf	$$⊢A\in V\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		vtoclgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		vtoclgf.2	$$⊢Ⅎx\psi$$
3		vtoclgf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		vtoclgf.4	$$⊢\phi$$
5		elex	$$⊢A\in V\to A\in \mathrm{V}$$
6	1	issetf	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$
7	4 3	mpbii	$$⊢x=A\to \psi$$
8	2 7	exlimi	$$⊢\exists xx=A\to \psi$$
9	6 8	sylbi	$$⊢A\in \mathrm{V}\to \psi$$
10	5 9	syl	$$⊢A\in V\to \psi$$