vtocldf

Description: Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	vtocld.1	$⊢ φ \to A \in V$
	vtocld.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
	vtocld.3	$⊢ φ \to ψ$
	vtocldf.4	$⊢ Ⅎ x φ$
	vtocldf.5	$⊢ φ \to \underline{Ⅎ} x A$
	vtocldf.6	$⊢ φ \to Ⅎ x χ$
Assertion	vtocldf	$⊢ φ \to χ$

Step	Hyp	Ref	Expression
1		vtocld.1	$⊢ φ \to A \in V$
2		vtocld.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
3		vtocld.3	$⊢ φ \to ψ$
4		vtocldf.4	$⊢ Ⅎ x φ$
5		vtocldf.5	$⊢ φ \to \underline{Ⅎ} x A$
6		vtocldf.6	$⊢ φ \to Ⅎ x χ$
7	2	ex	$⊢ φ \to (x = A \to (ψ \leftrightarrow χ))$
8	4 7	alrimi	$⊢ φ \to \forall x (x = A \to (ψ \leftrightarrow χ))$
9	4 3	alrimi	$⊢ φ \to \forall x ψ$
10		vtoclgft	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x χ) \land (\forall x (x = A \to (ψ \leftrightarrow χ)) \land \forall x ψ) \land A \in V) \to χ$
11	5 6 8 9 1 10	syl221anc	$⊢ φ \to χ$

Metamath Proof Explorer