Metamath Proof Explorer


Theorem mosubop

Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995)

Ref Expression
Hypothesis mosubop.1 * x φ
Assertion mosubop * x y z A = y z φ

Proof

Step Hyp Ref Expression
1 mosubop.1 * x φ
2 1 gen2 y z * x φ
3 mosubopt y z * x φ * x y z A = y z φ
4 2 3 ax-mp * x y z A = y z φ