Metamath Proof Explorer

Theorem dfralseu2

Description: The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 . (Contributed by David A. Wheeler, 21-Jul-2026)

		Ref	Expression
	Assertion	dfralseu2	$⊢ \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-reu	$⊢ \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-ralseu	$⊢ \forall\exists! x \in A (φ \to ψ) \leftrightarrow (\forall x \in A (φ \to ψ) \land \exists! x \in A φ)$
8		df-alseu	$⊢ \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 ψ)$