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

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	⊢ 𝐴 ∈ V
	Assertion	vtxval3sn	⊢ ( Vtx ‘ { { { 𝐴 } } } ) = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		vtxval3sn.a	⊢ 𝐴 ∈ V
2	1	opid	⊢ ⟨ 𝐴 , 𝐴 ⟩ = { { 𝐴 } }
3	2	eqcomi	⊢ { { 𝐴 } } = ⟨ 𝐴 , 𝐴 ⟩
4	3	sneqi	⊢ { { { 𝐴 } } } = { ⟨ 𝐴 , 𝐴 ⟩ }
5	1 4	vtxvalsnop	⊢ ( Vtx ‘ { { { 𝐴 } } } ) = { 𝐴 }