Description: "All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals . (Contributed by David A. Wheeler, 21-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ralseurals | ⊢ ( ∀∃! 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reurex | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) | |
| 2 | 1 | anim2i | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ) |
| 3 | df-ralseu | ⊢ ( ∀∃! 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) ) | |
| 4 | df-rals | ⊢ ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ) | |
| 5 | 2 3 4 | 3imtr4i | ⊢ ( ∀∃! 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) |