This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ V
Assertion iedgval3sn ⊢ iEdg ⁡ A = A

Proof

Step Hyp Ref Expression
1 vtxval3sn.a ⊢ A ∈ 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