Theorem iedgvalsnop

Description: Degenerated case 2 for edges: The set of indexed edges of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020) (Proof shortened by AV, 15-Jul-2022) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	vtxvalsnop.b	|- B e. _V
	vtxvalsnop.g	|- G = { <. B , B >. }
Assertion	iedgvalsnop	|- ( iEdg ` G ) = { B }

Proof

Step	Hyp	Ref	Expression
1		vtxvalsnop.b	|- B e. _V
2		vtxvalsnop.g	|- G = { <. B , B >. }
3	2	fveq2i	|- ( iEdg ` G ) = ( iEdg ` { <. B , B >. } )
4	1	snopeqopsnid	|- { <. B , B >. } = <. { B } , { B } >.
5	4	fveq2i	|- ( iEdg ` { <. B , B >. } ) = ( iEdg ` <. { B } , { B } >. )
6		snex	|- { B } e. _V
7	6 6	opiedgfvi	|- ( iEdg ` <. { B } , { B } >. ) = { B }
8	3 5 7	3eqtri	|- ( iEdg ` G ) = { B }