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	|- A e. _V
Assertion	iedgval3sn	|- ( iEdg ` { { { A } } } ) = { A }

Proof

Step	Hyp	Ref	Expression
1		vtxval3sn.a	|- A e. _V
2	1	opid	|- <. A , A >. = { { A } }
3	2	eqcomi	|- { { A } } = <. A , A >.
4	3	sneqi	|- { { { A } } } = { <. A , A >. }
5	1 4	iedgvalsnop	|- ( iEdg ` { { { A } } } ) = { A }