Theorem dfralseu2 51347

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

Assertion

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

Proof of Theorem dfralseu2

Step	Hyp	Ref	Expression
1		df-ral 3081	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
2		impexp 456	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
3	2	albii 1852	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
4	1, 3	bitr4i 281	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
5		df-reu 3370	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	4, 5	anbi12i 640	. 2 ⊢ ((∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ∧ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
7		df-ralseu 51346	. 2 ⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
8		df-alseu 51345	. 2 ⊢ (∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ↔ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ∧ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
9	6, 7, 8	3bitr4i 306	1 ⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2147  ∃!weu 2596  ∀wral 3080  ∃!wreu 3367  ∀∃!walseu 51343  ∀∃!wralseu 51344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081  df-reu 3370  df-alseu 51345  df-ralseu 51346

This theorem is used by: (None)