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

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 ⊢ 𝐵 ∈ V
moeq3.2 ⊢ 𝐶 ∈ V
moeq3.3 ⊢ ¬ ( 𝜑 ∧ 𝜓 )
Assertion moeq3 ∃* 𝑥 ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∨ ( ¬ ( 𝜑 ∨ 𝜓 ) ∧ 𝑥 = 𝐵 ) ∨ ( 𝜓 ∧ 𝑥 = 𝐶 ) )

Proof

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