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 e. _V
Assertion vtxval3sn
|- ( Vtx ` { { { 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 vtxvalsnop
 |-  ( Vtx ` { { { A } } } ) = { A }