Metamath Proof Explorer

Theorem dfrals2

Description: The bounded "all some" form is the general form with the class membership folded into the antecedent. (Contributed by David A. Wheeler, 22-Oct-2018) (Revised by David A. Wheeler, 12-Jul-2026)

		Ref	Expression
	Assertion	dfrals2	$⊢ \forall\exists x \in A (φ \to ψ) \leftrightarrow \forall\exists x ((x \in A \land φ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow \forall x (x \in A \to (φ \to ψ))$
2		impexp	$⊢ ((x \in A \land φ) \to ψ) \leftrightarrow (x \in A \to (φ \to ψ))$
3	2	albii	$⊢ \forall x ((x \in A \land φ) \to ψ) \leftrightarrow \forall x (x \in A \to (φ \to ψ))$
4	1 3	bitr4i	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow \forall x ((x \in A \land φ) \to ψ)$
5		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
6	4 5	anbi12i	$⊢ (\forall x \in A (φ \to ψ) \land \exists x \in A φ) \leftrightarrow (\forall x ((x \in A \land φ) \to ψ) \land \exists x (x \in A \land φ))$
7		df-rals	$⊢ \forall\exists x \in A (φ \to ψ) \leftrightarrow (\forall x \in A (φ \to ψ) \land \exists x \in A φ)$
8		df-als	$⊢ \forall\exists x ((x \in A \land φ) \to ψ) \leftrightarrow (\forall x ((x \in A \land φ) \to ψ) \land \exists x (x \in A \land φ))$
9	6 7 8	3bitr4i	$⊢ \forall\exists x \in A (φ \to ψ) \leftrightarrow \forall\exists x ((x \in A \land φ) \to ψ)$