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

Metamath Proof Explorer

Theorem vtocld

Description: Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 2-Sep-2024)

	Ref	Expression
Hypotheses	vtocld.1	$⊢ φ \to A \in V$
	vtocld.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
	vtocld.3	$⊢ φ \to ψ$
Assertion	vtocld	$⊢ φ \to χ$

Proof

Step	Hyp	Ref	Expression
1		vtocld.1	$⊢ φ \to A \in V$
2		vtocld.2	$⊢ (φ \land x = A) \to (ψ \leftrightarrow χ)$
3		vtocld.3	$⊢ φ \to ψ$
4		elisset	$⊢ A \in V \to \exists x x = A$
5	1 4	syl	$⊢ φ \to \exists x x = A$
6	3	adantr	$⊢ (φ \land x = A) \to ψ$
7	6 2	mpbid	$⊢ (φ \land x = A) \to χ$
8	5 7	exlimddv	$⊢ φ \to χ$