Theorem dfralseu2 50658

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

Assertion

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

Proof of Theorem dfralseu2

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2146  ∃!weu 2598  ∀wral 3081  ∃!wreu 3369  ∀∃!walseu 50654  ∀∃!wralseu 50655

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 3082  df-reu 3372  df-alseu 50656  df-ralseu 50657

This theorem is used by: (None)