Metamath Proof Explorer

Theorem uvtxval

Description: 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 uvtxval.v ⊢V=Vtx⁡G
Assertion uvtxval ⊢UnivVtx⁡G=v∈V|∀n∈V∖vn∈GNeighbVtxv

Proof

Step Hyp Ref Expression
1 uvtxval.v ⊢V=Vtx⁡G
2 df-uvtx ⊢UnivVtx=g∈V⟼v∈Vtx⁡g|∀n∈Vtx⁡g∖vn∈gNeighbVtxv
3 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
4 3 1 eqtr4di ⊢g=G→Vtx⁡g=V
5 4 difeq1d ⊢g=G→Vtx⁡g∖v=V∖v
6 oveq1 ⊢g=G→gNeighbVtxv=GNeighbVtxv
7 6 eleq2d ⊢g=G→n∈gNeighbVtxv↔n∈GNeighbVtxv
8 5 7 raleqbidv ⊢g=G→∀n∈Vtx⁡g∖vn∈gNeighbVtxv↔∀n∈V∖vn∈GNeighbVtxv
9 2 8 fvmptrabfv ⊢UnivVtx⁡G=v∈Vtx⁡G|∀n∈V∖vn∈GNeighbVtxv
10 1 eqcomi ⊢Vtx⁡G=V
11 10 rabeqi ⊢v∈Vtx⁡G|∀n∈V∖vn∈GNeighbVtxv=v∈V|∀n∈V∖vn∈GNeighbVtxv
12 9 11 eqtri ⊢UnivVtx⁡G=v∈V|∀n∈V∖vn∈GNeighbVtxv