r19.23t

Description: Closed theorem form of r19.23 . (Contributed by NM, 4-Mar-2013) (Revised by Mario Carneiro, 8-Oct-2016)

		Ref	Expression
	Assertion	r19.23t	$⊢ Ⅎ x ψ \to (\forall x \in A (φ \to ψ) \leftrightarrow (\exists x \in A φ \to ψ))$

Step	Hyp	Ref	Expression
1		19.23t	$⊢ Ⅎ x ψ \to (\forall x ((x \in A \land φ) \to ψ) \leftrightarrow (\exists x (x \in A \land φ) \to ψ))$
2		df-ral	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow \forall x (x \in A \to (φ \to ψ))$
3		impexp	$⊢ ((x \in A \land φ) \to ψ) \leftrightarrow (x \in A \to (φ \to ψ))$
4	3	albii	$⊢ \forall x ((x \in A \land φ) \to ψ) \leftrightarrow \forall x (x \in A \to (φ \to ψ))$
5	2 4	bitr4i	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow \forall x ((x \in A \land φ) \to ψ)$
6		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
7	6	imbi1i	$⊢ (\exists x \in A φ \to ψ) \leftrightarrow (\exists x (x \in A \land φ) \to ψ)$
8	1 5 7	3bitr4g	$⊢ Ⅎ x ψ \to (\forall x \in A (φ \to ψ) \leftrightarrow (\exists x \in A φ \to ψ))$

Metamath Proof Explorer