Metamath Proof Explorer

Theorem elsingles

Description: Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion elsingles ⊢ A ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 ↔ ∃ x A = x

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 → A ∈ V
2 snex ⊢ x ∈ V
3 eleq1 ⊢ A = x → A ∈ V ↔ x ∈ V
4 2 3 mpbiri ⊢ A = x → A ∈ V
5 4 exlimiv ⊢ ∃ x A = x → A ∈ V
6 eleq1 ⊢ y = A → y ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 ↔ A ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
7 eqeq1 ⊢ y = A → y = x ↔ A = x
8 7 exbidv ⊢ y = A → ∃ x y = x ↔ ∃ x A = x
9 df-singles ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = ran ⁡ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇
10 9 eleq2i ⊢ y ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 ↔ y ∈ ran ⁡ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇
11 vex ⊢ y ∈ V
12 11 elrn ⊢ y ∈ ran ⁡ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 ↔ ∃ x x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y
13 vex ⊢ x ∈ V
14 13 11 brsingle ⊢ x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y ↔ y = x
15 14 exbii ⊢ ∃ x x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y ↔ ∃ x y = x
16 10 12 15 3bitri ⊢ y ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 ↔ ∃ x y = x
17 6 8 16 vtoclbg ⊢ A ∈ V → A ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 ↔ ∃ x A = x
18 1 5 17 pm5.21nii ⊢ A ∈ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 ↔ ∃ x A = x