Theorem vtoclb

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993)

	Ref	Expression
Hypotheses	vtoclb.1	$$⊢A\in \mathrm{V}$$
	vtoclb.2	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
	vtoclb.3	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
	vtoclb.4	$$⊢\phi \leftrightarrow \psi$$
Assertion	vtoclb	$$⊢\chi \leftrightarrow \theta$$

Proof

Step	Hyp	Ref	Expression
1		vtoclb.1	$$⊢A\in \mathrm{V}$$
2		vtoclb.2	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
3		vtoclb.3	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
4		vtoclb.4	$$⊢\phi \leftrightarrow \psi$$
5	2 3	bibi12d	$$⊢x=A\to \left(\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\chi \leftrightarrow \theta \right)\right)$$
6	1 5 4	vtocl	$$⊢\chi \leftrightarrow \theta$$