This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mosub

Description: "At most one" remains true after substitution. (Contributed by NM, 9-Mar-1995)

Ref Expression
Hypothesis mosub.1 ⊢ ∃* 𝑥 𝜑
Assertion mosub ∃* 𝑥 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 )

Proof

Step Hyp Ref Expression
1 mosub.1 ⊢ ∃* 𝑥 𝜑
2 moeq ⊢ ∃* 𝑦 𝑦 = 𝐴
3 1 ax-gen ⊢ ∀ 𝑦 ∃* 𝑥 𝜑
4 moexexvw ⊢ ( ( ∃* 𝑦 𝑦 = 𝐴 ∧ ∀ 𝑦 ∃* 𝑥 𝜑 ) → ∃* 𝑥 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) )
5 2 3 4 mp2an ⊢ ∃* 𝑥 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 )