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

Metamath Proof Explorer

Theorem eueq2

Description: Equality has existential uniqueness (split into 2 cases). (Contributed by NM, 5-Apr-1995)

Ref Expression
Hypotheses eueq2.1 ⊢ 𝐴 ∈ V
eueq2.2 ⊢ 𝐵 ∈ V
Assertion eueq2 ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eueq2.1 ⊢ 𝐴 ∈ V
2 eueq2.2 ⊢ 𝐵 ∈ V
3 notnot ⊢ ( 𝜑 → ¬ ¬ 𝜑 )
4 1 eueqi ⊢ ∃! 𝑥 𝑥 = 𝐴
5 euanv ⊢ ( ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ( 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐴 ) )
6 5 biimpri ⊢ ( ( 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐴 ) → ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) )
7 4 6 mpan2 ⊢ ( 𝜑 → ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) )
8 euorv ⊢ ( ( ¬ ¬ 𝜑 ∧ ∃! 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) ) → ∃! 𝑥 ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
9 3 7 8 syl2anc ⊢ ( 𝜑 → ∃! 𝑥 ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
10 orcom ⊢ ( ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ¬ 𝜑 ) )
11 3 bianfd ⊢ ( 𝜑 → ( ¬ 𝜑 ↔ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
12 11 orbi2d ⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ¬ 𝜑 ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
13 10 12 bitrid ⊢ ( 𝜑 → ( ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
14 13 eubidv ⊢ ( 𝜑 → ( ∃! 𝑥 ( ¬ 𝜑 ∨ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) ↔ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
15 9 14 mpbid ⊢ ( 𝜑 → ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
16 2 eueqi ⊢ ∃! 𝑥 𝑥 = 𝐵
17 euanv ⊢ ( ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ↔ ( ¬ 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐵 ) )
18 17 biimpri ⊢ ( ( ¬ 𝜑 ∧ ∃! 𝑥 𝑥 = 𝐵 ) → ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )
19 16 18 mpan2 ⊢ ( ¬ 𝜑 → ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )
20 euorv ⊢ ( ( ¬ 𝜑 ∧ ∃! 𝑥 ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) → ∃! 𝑥 ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
21 19 20 mpdan ⊢ ( ¬ 𝜑 → ∃! 𝑥 ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
22 id ⊢ ( ¬ 𝜑 → ¬ 𝜑 )
23 22 bianfd ⊢ ( ¬ 𝜑 → ( 𝜑 ↔ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
24 23 orbi1d ⊢ ( ¬ 𝜑 → ( ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
25 24 eubidv ⊢ ( ¬ 𝜑 → ( ∃! 𝑥 ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ↔ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) ) )
26 21 25 mpbid ⊢ ( ¬ 𝜑 → ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) ) )
27 15 26 pm2.61i ⊢ ∃! 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 = 𝐵 ) )