vtoclgft

Description: Closed theorem form of vtoclgf . (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 Gino Giotto, 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		elisset	$⊢ A \in V \to \exists z z = A$
2		nfv	$⊢ Ⅎ z \underline{Ⅎ} x A$
3		nfnfc1	$⊢ Ⅎ x \underline{Ⅎ} x A$
4		nfcvd	$⊢ \underline{Ⅎ} x A \to \underline{Ⅎ} x z$
5		id	$⊢ \underline{Ⅎ} x A \to \underline{Ⅎ} x A$
6	4 5	nfeqd	$⊢ \underline{Ⅎ} x A \to Ⅎ x z = A$
7	6	nfnd	$⊢ \underline{Ⅎ} x A \to Ⅎ x \neg z = A$
8		nfvd	$⊢ \underline{Ⅎ} x A \to Ⅎ z \neg x = A$
9		eqeq1	$⊢ z = x \to (z = A \leftrightarrow x = A)$
10	9	a1i	$⊢ \underline{Ⅎ} x A \to (z = x \to (z = A \leftrightarrow x = A))$
11		notbi	$⊢ (z = A \leftrightarrow x = A) \leftrightarrow (\neg z = A \leftrightarrow \neg x = A)$
12	10 11	syl6ib	$⊢ \underline{Ⅎ} x A \to (z = x \to (\neg z = A \leftrightarrow \neg x = A))$
13		biimp	$⊢ (\neg z = A \leftrightarrow \neg x = A) \to (\neg z = A \to \neg x = A)$
14	12 13	syl6	$⊢ \underline{Ⅎ} x A \to (z = x \to (\neg z = A \to \neg x = A))$
15	2 3 7 8 14	cbv1v	$⊢ \underline{Ⅎ} x A \to (\forall z \neg z = A \to \forall x \neg x = A)$
16		equcomi	$⊢ x = z \to z = x$
17		biimpr	$⊢ (\neg z = A \leftrightarrow \neg x = A) \to (\neg x = A \to \neg z = A)$
18	16 12 17	syl56	$⊢ \underline{Ⅎ} x A \to (x = z \to (\neg x = A \to \neg z = A))$
19	3 2 8 7 18	cbv1v	$⊢ \underline{Ⅎ} x A \to (\forall x \neg x = A \to \forall z \neg z = A)$
20	15 19	impbid	$⊢ \underline{Ⅎ} x A \to (\forall z \neg z = A \leftrightarrow \forall x \neg x = A)$
21		alnex	$⊢ \forall z \neg z = A \leftrightarrow \neg \exists z z = A$
22		alnex	$⊢ \forall x \neg x = A \leftrightarrow \neg \exists x x = A$
23	20 21 22	3bitr3g	$⊢ \underline{Ⅎ} x A \to (\neg \exists z z = A \leftrightarrow \neg \exists x x = A)$
24	23	con4bid	$⊢ \underline{Ⅎ} x A \to (\exists z z = A \leftrightarrow \exists x x = A)$
25	1 24	syl5ib	$⊢ \underline{Ⅎ} x A \to (A \in V \to \exists x x = A)$
26	25	ad2antrr	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ)) \to (A \in V \to \exists x x = A)$
27	26	3impia	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ) \land A \in V) \to \exists x x = A$
28		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
29	28	imim2i	$⊢ (x = A \to (φ \leftrightarrow ψ)) \to (x = A \to (φ \to ψ))$
30	29	com23	$⊢ (x = A \to (φ \leftrightarrow ψ)) \to (φ \to (x = A \to ψ))$
31	30	imp	$⊢ ((x = A \to (φ \leftrightarrow ψ)) \land φ) \to (x = A \to ψ)$
32	31	alanimi	$⊢ (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ) \to \forall x (x = A \to ψ)$
33		19.23t	$⊢ Ⅎ x ψ \to (\forall x (x = A \to ψ) \leftrightarrow (\exists x x = A \to ψ))$
34	33	adantl	$⊢ (\underline{Ⅎ} x A \land Ⅎ x ψ) \to (\forall x (x = A \to ψ) \leftrightarrow (\exists x x = A \to ψ))$
35	32 34	syl5ib	$⊢ (\underline{Ⅎ} x A \land Ⅎ x ψ) \to ((\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ) \to (\exists x x = A \to ψ))$
36	35	imp	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ)) \to (\exists x x = A \to ψ)$
37	36	3adant3	$⊢ ((\underline{Ⅎ} x A \land Ⅎ x ψ) \land (\forall x (x = A \to (φ \leftrightarrow ψ)) \land \forall x φ) \land A \in V) \to (\exists x x = A \to ψ)$
38	27 37	mpd	$⊢ ((\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