P. 168 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16701-16701   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	alsc2d 16701	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)

< Previous  Wrap >