Metamath Proof Explorer


Theorem vtxval3sn

Description: Degenerated case 3 for vertices: The set of vertices 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 vtxval3sn Vtx 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 vtxvalsnop Vtx A = A