Metamath Proof Explorer

Theorem uvtxusgr

Description: The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

Ref Expression
Hypotheses uvtxnbgr.v ⊢V=Vtx⁡G
uvtxusgr.e ⊢E=Edg⁡G
Assertion uvtxusgr ⊢G∈USGraph→UnivVtx⁡G=n∈V|∀k∈V∖nkn∈E

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v ⊢V=Vtx⁡G
2 uvtxusgr.e ⊢E=Edg⁡G
3 1 uvtxval ⊢UnivVtx⁡G=n∈V|∀k∈V∖nk∈GNeighbVtxn
4 2 nbusgreledg ⊢G∈USGraph→k∈GNeighbVtxn↔kn∈E
5 4 ralbidv ⊢G∈USGraph→∀k∈V∖nk∈GNeighbVtxn↔∀k∈V∖nkn∈E
6 5 rabbidv ⊢G∈USGraph→n∈V|∀k∈V∖nk∈GNeighbVtxn=n∈V|∀k∈V∖nkn∈E
7 3 6 eqtrid ⊢G∈USGraph→UnivVtx⁡G=n∈V|∀k∈V∖nkn∈E