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	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )