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

Metamath Proof Explorer

Theorem fvsingle

Description: The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Revised by Scott Fenton, 13-Apr-2018)

Ref Expression
Assertion fvsingle ( Singleton ‘ 𝐴 ) = { 𝐴 }

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = 𝐴 → ( Singleton ‘ 𝑥 ) = ( Singleton ‘ 𝐴 ) )
2 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
3 1 2 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( Singleton ‘ 𝑥 ) = { 𝑥 } ↔ ( Singleton ‘ 𝐴 ) = { 𝐴 } ) )
4 eqid ⊢ { 𝑥 } = { 𝑥 }
5 vex ⊢ 𝑥 ∈ V
6 vsnex ⊢ { 𝑥 } ∈ V
7 5 6 brsingle ⊢ ( 𝑥 Singleton { 𝑥 } ↔ { 𝑥 } = { 𝑥 } )
8 4 7 mpbir ⊢ 𝑥 Singleton { 𝑥 }
9 fnsingle ⊢ Singleton Fn V
10 fnbrfvb ⊢ ( ( Singleton Fn V ∧ 𝑥 ∈ V ) → ( ( Singleton ‘ 𝑥 ) = { 𝑥 } ↔ 𝑥 Singleton { 𝑥 } ) )
11 9 5 10 mp2an ⊢ ( ( Singleton ‘ 𝑥 ) = { 𝑥 } ↔ 𝑥 Singleton { 𝑥 } )
12 8 11 mpbir ⊢ ( Singleton ‘ 𝑥 ) = { 𝑥 }
13 3 12 vtoclg ⊢ ( 𝐴 ∈ V → ( Singleton ‘ 𝐴 ) = { 𝐴 } )
14 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( Singleton ‘ 𝐴 ) = ∅ )
15 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
16 15 biimpi ⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
17 14 16 eqtr4d ⊢ ( ¬ 𝐴 ∈ V → ( Singleton ‘ 𝐴 ) = { 𝐴 } )
18 13 17 pm2.61i ⊢ ( Singleton ‘ 𝐴 ) = { 𝐴 }