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

Metamath Proof Explorer

Theorem uvtxnbgrss

Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 30-Oct-2020)

		Ref	Expression
	Hypothesis	uvtxel.v	$⊢ V = Vtx (G)$
	Assertion	uvtxnbgrss	$⊢ N \in UnivVtx (G) \to V ∖ \{N\} \subseteq G NeighbVtx N$

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	$⊢ V = Vtx (G)$
2	1	vtxnbuvtx	$⊢ N \in UnivVtx (G) \to \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N)$
3		dfss3	$⊢ V ∖ \{N\} \subseteq G NeighbVtx N \leftrightarrow \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N)$
4	2 3	sylibr	$⊢ N \in UnivVtx (G) \to V ∖ \{N\} \subseteq G NeighbVtx N$