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 ⊢ ∃* x ∈ A φ

Proof

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