Metamath Proof Explorer

Theorem mopickr

Description: "At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 ( pm2.21 ) and *14.26 ( eupickbi ) from WhiteheadRussell p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024) (Proof modification is discouraged.)

Ref Expression
Assertion mopickr ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ → ψ → φ

Proof

Step Hyp Ref Expression
1 exancom ⊢ ∃ x φ ∧ ψ ↔ ∃ x ψ ∧ φ
2 moeu2 ⊢ ∃* x ψ ↔ ¬ ∃ x ψ ∨ ∃! x ψ
3 19.8a ⊢ ψ → ∃ x ψ
4 3 con3i ⊢ ¬ ∃ x ψ → ¬ ψ
5 pm2.21 ⊢ ¬ ψ → ψ → φ
6 4 5 syl ⊢ ¬ ∃ x ψ → ψ → φ
7 6 a1d ⊢ ¬ ∃ x ψ → ∃ x ψ ∧ φ → ψ → φ
8 eupickbi ⊢ ∃! x ψ → ∃ x ψ ∧ φ ↔ ∀ x ψ → φ
9 sp ⊢ ∀ x ψ → φ → ψ → φ
10 8 9 biimtrdi ⊢ ∃! x ψ → ∃ x ψ ∧ φ → ψ → φ
11 7 10 jaoi ⊢ ¬ ∃ x ψ ∨ ∃! x ψ → ∃ x ψ ∧ φ → ψ → φ
12 2 11 sylbi ⊢ ∃* x ψ → ∃ x ψ ∧ φ → ψ → φ
13 1 12 biimtrid ⊢ ∃* x ψ → ∃ x φ ∧ ψ → ψ → φ
14 13 imp ⊢ ∃* x ψ ∧ ∃ x φ ∧ ψ → ψ → φ