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 ⊢ A ∈ V
eueq2.2 ⊢ B ∈ V
Assertion eueq2 ⊢ ∃! x φ ∧ x = A ∨ ¬ φ ∧ x = B

Proof

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