Metamath Proof Explorer

Theorem cplgruvtxb

Description: A graph G is complete iff each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 15-Feb-2022)

Ref Expression
Hypothesis cplgruvtxb.v ⊢ V = Vtx ⁡ G
Assertion cplgruvtxb ⊢ G ∈ W → G ∈ ComplGraph ↔ UnivVtx ⁡ G = V

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢ V = Vtx ⁡ G
2 fveq2 ⊢ g = G → UnivVtx ⁡ g = UnivVtx ⁡ G
3 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
4 3 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
5 2 4 eqeq12d ⊢ g = G → UnivVtx ⁡ g = Vtx ⁡ g ↔ UnivVtx ⁡ G = V
6 df-cplgr ⊢ ComplGraph = g | UnivVtx ⁡ g = Vtx ⁡ g
7 5 6 elab2g ⊢ G ∈ W → G ∈ ComplGraph ↔ UnivVtx ⁡ G = V