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 ax12ev2 x x = y ψ x = y ψ
6 4 5 syl6 x φ x = y x φ ψ x = y ψ
7 2 6 syl5d x φ x = y x φ ψ φ ψ
8 7 exlimiv y x φ x = y x φ ψ φ ψ
9 1 8 sylbi * x φ x φ ψ φ ψ
10 9 imp * x φ x φ ψ φ ψ