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	⊢ ∃* 𝑥 ∈ { 𝐴 } 𝜑