This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfeu

Description: Rederive df-eu from the old definition eu6 . (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 25-May-2019) (Proof shortened by BJ, 7-Oct-2022) (Proof modification is discouraged.) Use df-eu instead. (New usage is discouraged.)

Ref Expression
Assertion dfeu ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )

Proof

Step Hyp Ref Expression
1 abai ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜑 ∧ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ) )
2 euex ⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 𝜑 )
3 2 pm4.71ri ⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃! 𝑥 𝜑 ) )
4 moeu ⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
5 4 anbi2i ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜑 ∧ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ) )
6 1 3 5 3bitr4i ⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )