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