Metamath Proof Explorer

Theorem moeq3

Description: "At most one" property of equality (split into 3 cases). (The first two hypotheses could be eliminated with longer proof.) (Contributed by NM, 23-Apr-1995)

Ref Expression
Hypotheses moeq3.1 ⊢ B ∈ V
moeq3.2 ⊢ C ∈ V
moeq3.3 ⊢ ¬ φ ∧ ψ
Assertion moeq3 ⊢ ∃* x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C

Proof

Step Hyp Ref Expression
1 moeq3.1 ⊢ B ∈ V
2 moeq3.2 ⊢ C ∈ V
3 moeq3.3 ⊢ ¬ φ ∧ ψ
4 eqeq2 ⊢ y = A → x = y ↔ x = A
5 4 anbi2d ⊢ y = A → φ ∧ x = y ↔ φ ∧ x = A
6 biidd ⊢ y = A → ¬ φ ∨ ψ ∧ x = B ↔ ¬ φ ∨ ψ ∧ x = B
7 biidd ⊢ y = A → ψ ∧ x = C ↔ ψ ∧ x = C
8 5 6 7 3orbi123d ⊢ y = A → φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
9 8 eubidv ⊢ y = A → ∃! x φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
10 vex ⊢ y ∈ V
11 10 1 2 3 eueq3 ⊢ ∃! x φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
12 9 11 vtoclg ⊢ A ∈ V → ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
13 eumo ⊢ ∃! x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → ∃* x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
14 12 13 syl ⊢ A ∈ V → ∃* x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
15 eqvisset ⊢ x = A → A ∈ V
16 pm2.21 ⊢ ¬ A ∈ V → A ∈ V → x = y
17 15 16 syl5 ⊢ ¬ A ∈ V → x = A → x = y
18 17 anim2d ⊢ ¬ A ∈ V → φ ∧ x = A → φ ∧ x = y
19 18 orim1d ⊢ ¬ A ∈ V → φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
20 3orass ⊢ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
21 3orass ⊢ φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C ↔ φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
22 19 20 21 3imtr4g ⊢ ¬ A ∈ V → φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
23 22 alrimiv ⊢ ¬ A ∈ V → ∀ x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
24 euimmo ⊢ ∀ x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → ∃! x φ ∧ x = y ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C → ∃* x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
25 23 11 24 mpisyl ⊢ ¬ A ∈ V → ∃* x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C
26 14 25 pm2.61i ⊢ ∃* x φ ∧ x = A ∨ ¬ φ ∨ ψ ∧ x = B ∨ ψ ∧ x = C