Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mosubop.1 | ⊢ ∃* 𝑥 𝜑 | |
Assertion | mosubop | ⊢ ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mosubop.1 | ⊢ ∃* 𝑥 𝜑 | |
2 | 1 | gen2 | ⊢ ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 |
3 | mosubopt | ⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) ) | |
4 | 2 3 | ax-mp | ⊢ ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = 〈 𝑦 , 𝑧 〉 ∧ 𝜑 ) |