Theorem dfralseu2 50601

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 50568. (Contributed by David A. Wheeler, 21-Jul-2026.)

Assertion

Ref	Expression
dfralseu2	⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))

Proof of Theorem dfralseu2

Step	Hyp	Ref	Expression
1		df-ral 3080	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
2		impexp 455	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
3	2	albii 1849	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
4	1, 3	bitr4i 281	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
5		df-reu 3370	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	4, 5	anbi12i 639	. 2 ⊢ ((∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ∧ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
7		df-ralseu 50600	. 2 ⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
8		df-alseu 50599	. 2 ⊢ (∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ↔ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ∧ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
9	6, 7, 8	3bitr4i 306	1 ⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   ∈ wcel 2143  ∃!weu 2596  ∀wral 3079  ∃!wreu 3367  ∀∃!walseu 50597  ∀∃!wralseu 50598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080  df-reu 3370  df-alseu 50599  df-ralseu 50600

This theorem is referenced by: (None)