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 ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A = A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ x = A → 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ x = 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A
2 sneq ⊢ x = A → x = A
3 1 2 eqeq12d ⊢ x = A → 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ x = x ↔ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A = A
4 eqid ⊢ x = x
5 vex ⊢ x ∈ V
6 vsnex ⊢ x ∈ V
7 5 6 brsingle ⊢ x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x ↔ x = x
8 4 7 mpbir ⊢ x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x
9 fnsingle ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 Fn V
10 fnbrfvb ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 Fn V ∧ x ∈ V → 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ x = x ↔ x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x
11 9 5 10 mp2an ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ x = x ↔ x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x
12 8 11 mpbir ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ x = x
13 3 12 vtoclg ⊢ A ∈ V → 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A = A
14 fvprc ⊢ ¬ A ∈ V → 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A = ∅
15 snprc ⊢ ¬ A ∈ V ↔ A = ∅
16 15 biimpi ⊢ ¬ A ∈ V → A = ∅
17 14 16 eqtr4d ⊢ ¬ A ∈ V → 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A = A
18 13 17 pm2.61i ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ⁡ A = A