Metamath Proof Explorer

Theorem uvtxel

Description: A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 29-Oct-2020) (Revised by AV, 14-Feb-2022)

		Ref	Expression
	Hypothesis	uvtxel.v	$⊢ V = Vtx (G)$
	Assertion	uvtxel	$⊢ N \in UnivVtx (G) \leftrightarrow (N \in V \land \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N))$

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	$⊢ V = Vtx (G)$
2		sneq	$⊢ v = N \to \{v\} = \{N\}$
3	2	difeq2d	$⊢ v = N \to V ∖ \{v\} = V ∖ \{N\}$
4		oveq2	$⊢ v = N \to G NeighbVtx v = G NeighbVtx N$
5	4	eleq2d	$⊢ v = N \to (n \in (G NeighbVtx v) \leftrightarrow n \in (G NeighbVtx N))$
6	3 5	raleqbidv	$⊢ v = N \to (\forall n \in (V ∖ \{v\}) n \in (G NeighbVtx v) \leftrightarrow \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N))$
7	1	uvtxval	$⊢ UnivVtx (G) = \{v \in V \| \forall n \in (V ∖ \{v\}) n \in (G NeighbVtx v)\}$
8	6 7	elrab2	$⊢ N \in UnivVtx (G) \leftrightarrow (N \in V \land \forall n \in (V ∖ \{N\}) n \in (G NeighbVtx N))$