Metamath Proof Explorer


Theorem mopick

Description: "At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997) (Proof shortened by Wolf Lammen, 17-Sep-2019)

Ref Expression
Assertion mopick * x φ x φ ψ φ ψ

Proof

Step Hyp Ref Expression
1 df-mo * x φ y x φ x = y
2 sp x φ x = y φ x = y
3 pm3.45 φ x = y φ ψ x = y ψ
4 3 aleximi x φ x = y x φ ψ x x = y ψ
5 sbalex x x = y ψ x x = y ψ
6 sp x x = y ψ x = y ψ
7 5 6 sylbi x x = y ψ x = y ψ
8 4 7 syl6 x φ x = y x φ ψ x = y ψ
9 2 8 syl5d x φ x = y x φ ψ φ ψ
10 9 exlimiv y x φ x = y x φ ψ φ ψ
11 1 10 sylbi * x φ x φ ψ φ ψ
12 11 imp * x φ x φ ψ φ ψ