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 ⊢∃!xx=A
5 euanv ⊢∃!xφ∧x=A↔φ∧∃!xx=A
6 5 biimpri ⊢φ∧∃!xx=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 ⊢∃!xx=B
17 euanv ⊢∃!x¬φ∧x=B↔¬φ∧∃!xx=B
18 17 biimpri ⊢¬φ∧∃!xx=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