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 ‘ { { { 𝐴 } } } ) = { 𝐴 }