ceqsalt

Description: Closed theorem version of ceqsalg . (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 10-Oct-2016)

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

Step	Hyp	Ref	Expression
1		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
2	1	imim3i	$⊢ (x = A \to (φ \leftrightarrow ψ)) \to ((x = A \to φ) \to (x = A \to ψ))$
3	2	al2imi	$⊢ \forall x (x = A \to (φ \leftrightarrow ψ)) \to (\forall x (x = A \to φ) \to \forall x (x = A \to ψ))$
4		elisset	$⊢ A \in V \to \exists x x = A$
5		19.23t	$⊢ Ⅎ x ψ \to (\forall x (x = A \to ψ) \leftrightarrow (\exists x x = A \to ψ))$
6	5	biimpd	$⊢ Ⅎ x ψ \to (\forall x (x = A \to ψ) \to (\exists x x = A \to ψ))$
7	4 6	syl7	$⊢ Ⅎ x ψ \to (\forall x (x = A \to ψ) \to (A \in V \to ψ))$
8	3 7	sylan9r	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (\forall x (x = A \to φ) \to (A \in V \to ψ))$
9	8	com23	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (A \in V \to (\forall x (x = A \to φ) \to ψ))$
10	9	3impia	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \leftrightarrow ψ)) \land A \in V) \to (\forall x (x = A \to φ) \to ψ)$
11		ceqsal1t	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (ψ \to \forall x (x = A \to φ))$
12	11	3adant3	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \leftrightarrow ψ)) \land A \in V) \to (ψ \to \forall x (x = A \to φ))$
13	10 12	impbid	$⊢ (Ⅎ x ψ \land \forall x (x = A \to (φ \leftrightarrow ψ)) \land A \in V) \to (\forall x (x = A \to φ) \leftrightarrow ψ)$

Metamath Proof Explorer