Theorem alseueu 50615

Description: "The 𝜑 is 𝜓 " implies that exactly one thing is both 𝜑 and 𝜓. This is the half of dfalseu2 50614 that drops the universal conjunct; it does not reverse, so ∃!𝑥(𝜑 ∧ 𝜓) cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 21-Jul-2026.)

Assertion

Ref	Expression
alseueu	⊢ (∀∃!𝑥(𝜑 → 𝜓) → ∃!𝑥(𝜑 ∧ 𝜓))

Proof of Theorem alseueu

Step	Hyp	Ref	Expression
1		dfalseu2 50614	. 2 ⊢ (∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥(𝜑 ∧ 𝜓)))
2	1	simprbi 502	1 ⊢ (∀∃!𝑥(𝜑 → 𝜓) → ∃!𝑥(𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1568  ∃!weu 2596  ∀∃!walseu 50597

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-alseu 50599

This theorem is referenced by: (None)