r19.35

Description: Restricted quantifier version of 19.35 . (Contributed by NM, 20-Sep-2003) (Proof shortened by Wolf Lammen, 22-Dec-2024)

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

Step	Hyp	Ref	Expression
1		pm5.5	$⊢ φ \to ((φ \to ψ) \leftrightarrow ψ)$
2	1	ralrexbid	$⊢ \forall x \in A φ \to (\exists x \in A (φ \to ψ) \leftrightarrow \exists x \in A ψ)$
3	2	biimpcd	$⊢ \exists x \in A (φ \to ψ) \to (\forall x \in A φ \to \exists x \in A ψ)$
4		rexnal	$⊢ \exists x \in A \neg φ \leftrightarrow \neg \forall x \in A φ$
5		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
6	5	reximi	$⊢ \exists x \in A \neg φ \to \exists x \in A (φ \to ψ)$
7	4 6	sylbir	$⊢ \neg \forall x \in A φ \to \exists x \in A (φ \to ψ)$
8		ax-1	$⊢ ψ \to (φ \to ψ)$
9	8	reximi	$⊢ \exists x \in A ψ \to \exists x \in A (φ \to ψ)$
10	7 9	ja	$⊢ (\forall x \in A φ \to \exists x \in A ψ) \to \exists x \in A (φ \to ψ)$
11	3 10	impbii	$⊢ \exists x \in A (φ \to ψ) \leftrightarrow (\forall x \in A φ \to \exists x \in A ψ)$

Metamath Proof Explorer