Metamath Proof Explorer

Theorem moexex

Description: "At most one" double quantification. Usage of this theorem is discouraged because it depends on ax-13 . Use the version moexexvw when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 28-Dec-2018) Factor out common proof lines with moexexvw . (Revised by Wolf Lammen, 2-Oct-2023) (New usage is discouraged.)

Ref Expression
Hypothesis moexex.1 y φ
Assertion moexex * x φ x * y ψ * y x φ ψ


Step Hyp Ref Expression
1 moexex.1 y φ
2 1 nfmo y * x φ
3 nfe1 x x φ ψ
4 3 nfmo x * y x φ ψ
5 1 2 4 moexexlem * x φ x * y ψ * y x φ ψ