vtoclgft

Description: Closed theorem form of vtoclgf . The reverse implication is proven in ceqsal1t . See ceqsalt for a version with x and A disjoint. (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) Avoid ax-13 . (Revised by GG, 6-Oct-2023)

		Ref	Expression
	Assertion	vtoclgft	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ) \land A \in V) \to ψ$

Proof

Step	Hyp	Ref	Expression
1		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
2	1	imim2i	$⊢ (x = A \to (φ \leftrightarrow ψ)) \to (x = A \to (φ \to ψ))$
3	2	alimi	$⊢ \forall x (x = A \to (φ \leftrightarrow ψ)) \to \forall x (x = A \to (φ \to ψ))$
4		spcimgft	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land \forall x (x = A \to (φ \to ψ))) \to (A \in V \to (\forall x φ \to ψ))$
5	3 4	sylan2	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (A \in V \to (\forall x φ \to ψ))$
6	5	com23	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (\forall x φ \to (A \in V \to ψ))$
7	6	impr	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ)) \to (A \in V \to ψ)$
8	7	3impia	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ) \land A \in V) \to ψ$

Metamath Proof Explorer

Theorem vtoclgft

Proof