Metamath Proof Explorer


Theorem iedgval3sn

Description: Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Hypothesis vtxval3sn.a 𝐴 ∈ V
Assertion iedgval3sn ( iEdg ‘ { { { 𝐴 } } } ) = { 𝐴 }

Proof

Step Hyp Ref Expression
1 vtxval3sn.a 𝐴 ∈ V
2 1 opid 𝐴 , 𝐴 ⟩ = { { 𝐴 } }
3 2 eqcomi { { 𝐴 } } = ⟨ 𝐴 , 𝐴
4 3 sneqi { { { 𝐴 } } } = { ⟨ 𝐴 , 𝐴 ⟩ }
5 1 4 iedgvalsnop ( iEdg ‘ { { { 𝐴 } } } ) = { 𝐴 }