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

Metamath Proof Explorer

Theorem dfeumo

Description: An elementary proof showing the reverse direction of dfmoeu . Here the characterizing expression of existential uniqueness ( eu6 ) is derived from that of uniqueness ( df-mo ). (Contributed by Wolf Lammen, 3-Oct-2023)

Ref Expression
Assertion dfeumo ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 ax6ev ⊢ ∃ 𝑥 𝑥 = 𝑦
2 biimpr ⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
3 2 aleximi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜑 ) )
4 1 3 mpi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑥 𝜑 )
5 4 exlimiv ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑥 𝜑 )
6 5 pm4.71ri ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
7 abai ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ↔ ( ∃ 𝑥 𝜑 ∧ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) )
8 dfmoeu ⊢ ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
9 8 anbi2i ⊢ ( ( ∃ 𝑥 𝜑 ∧ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) ↔ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
10 6 7 9 3bitrri ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )