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 ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N

Proof

Step Hyp Ref Expression
1 uvtxel.v ⊢ V = Vtx ⁡ G
2 sneq ⊢ v = N → v = N
3 2 difeq2d ⊢ v = N → V ∖ v = V ∖ N
4 oveq2 ⊢ v = N → G NeighbVtx v = G NeighbVtx N
5 4 eleq2d ⊢ v = N → n ∈ G NeighbVtx v ↔ n ∈ G NeighbVtx N
6 3 5 raleqbidv ⊢ v = N → ∀ n ∈ V ∖ v n ∈ G NeighbVtx v ↔ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
7 1 uvtxval ⊢ UnivVtx ⁡ G = v ∈ V | ∀ n ∈ V ∖ v n ∈ G NeighbVtx v
8 6 7 elrab2 ⊢ N ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N