vtoclegft

Description: Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef .) (Contributed by NM, 7-Nov-2005) (Revised by Mario Carneiro, 11-Oct-2016) (Proof shortened by Wolf Lammen, 26-Jan-2025)

		Ref	Expression
	Assertion	vtoclegft	$⊢ (A \in B \land Ⅎ x φ \land \forall x (x = A \to φ)) \to φ$

Proof

Step	Hyp	Ref	Expression
1		biidd	$⊢ x = A \to (φ \leftrightarrow φ)$
2	1	ax-gen	$⊢ \forall x (x = A \to (φ \leftrightarrow φ))$
3		ceqsalt	$⊢ (Ⅎ x φ \land \forall x (x = A \to (φ \leftrightarrow φ)) \land A \in B) \to (\forall x (x = A \to φ) \leftrightarrow φ)$
4	2 3	mp3an2	$⊢ (Ⅎ x φ \land A \in B) \to (\forall x (x = A \to φ) \leftrightarrow φ)$
5	4	ancoms	$⊢ (A \in B \land Ⅎ x φ) \to (\forall x (x = A \to φ) \leftrightarrow φ)$
6	5	biimpd	$⊢ (A \in B \land Ⅎ x φ) \to (\forall x (x = A \to φ) \to φ)$
7	6	3impia	$⊢ (A \in B \land Ⅎ x φ \land \forall x (x = A \to φ)) \to φ$

Metamath Proof Explorer

Theorem vtoclegft

Proof