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

Metamath Proof Explorer

Theorem rmosn

Description: A restricted at-most-one quantifier over a singleton is always true. (Contributed by AV, 3-Apr-2023)

Ref Expression
Assertion rmosn ∃* 𝑥 ∈ { 𝐴 } 𝜑

Proof

Step Hyp Ref Expression
1 idd ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
2 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝜑
3 sbceq1a ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
4 2 3 rexsngf ⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
5 2 3 reusngf ⊢ ( 𝐴 ∈ V → ( ∃! 𝑥 ∈ { 𝐴 } 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
6 1 4 5 3imtr4d ⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 → ∃! 𝑥 ∈ { 𝐴 } 𝜑 ) )
7 rmo5 ⊢ ( ∃* 𝑥 ∈ { 𝐴 } 𝜑 ↔ ( ∃ 𝑥 ∈ { 𝐴 } 𝜑 → ∃! 𝑥 ∈ { 𝐴 } 𝜑 ) )
8 6 7 sylibr ⊢ ( 𝐴 ∈ V → ∃* 𝑥 ∈ { 𝐴 } 𝜑 )
9 rmo0 ⊢ ∃* 𝑥 ∈ ∅ 𝜑
10 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
11 rmoeq1 ⊢ ( { 𝐴 } = ∅ → ( ∃* 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∃* 𝑥 ∈ ∅ 𝜑 ) )
12 10 11 sylbi ⊢ ( ¬ 𝐴 ∈ V → ( ∃* 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∃* 𝑥 ∈ ∅ 𝜑 ) )
13 9 12 mpbiri ⊢ ( ¬ 𝐴 ∈ V → ∃* 𝑥 ∈ { 𝐴 } 𝜑 )
14 8 13 pm2.61i ⊢ ∃* 𝑥 ∈ { 𝐴 } 𝜑