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\in \mathrm{V}$$
	vtxvalsnop.g	$$⊢G=\left\{⟨B,B⟩\right\}$$
Assertion	iedgvalsnop	$$⊢\mathrm{iEdg}\left(G\right)=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vtxvalsnop.b	$$⊢B\in \mathrm{V}$$
2		vtxvalsnop.g	$$⊢G=\left\{⟨B,B⟩\right\}$$
3	2	fveq2i	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(\left\{⟨B,B⟩\right\}\right)$$
4	1	snopeqopsnid	$$⊢\left\{⟨B,B⟩\right\}=⟨\left\{B\right\},\left\{B\right\}⟩$$
5	4	fveq2i	$$⊢\mathrm{iEdg}\left(\left\{⟨B,B⟩\right\}\right)=\mathrm{iEdg}\left(⟨\left\{B\right\},\left\{B\right\}⟩\right)$$
6		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
7	6 6	opiedgfvi	$$⊢\mathrm{iEdg}\left(⟨\left\{B\right\},\left\{B\right\}⟩\right)=\left\{B\right\}$$
8	3 5 7	3eqtri	$$⊢\mathrm{iEdg}\left(G\right)=\left\{B\right\}$$