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 ∃* 𝑥 𝜑
Assertion mosubop ∃* 𝑥𝑦𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )

Proof

Step Hyp Ref Expression
1 mosubop.1 ∃* 𝑥 𝜑
2 1 gen2 𝑦𝑧 ∃* 𝑥 𝜑
3 mosubopt ( ∀ 𝑦𝑧 ∃* 𝑥 𝜑 → ∃* 𝑥𝑦𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )
4 2 3 ax-mp ∃* 𝑥𝑦𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )