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 \in W \to (G \in ComplGraph \leftrightarrow UnivVtx (G) = V)$

Proof

Step	Hyp	Ref	Expression
1		cplgruvtxb.v	$⊢ V = Vtx (G)$
2		fveq2	$⊢ g = G \to UnivVtx (g) = UnivVtx (G)$
3		fveq2	$⊢ g = G \to Vtx (g) = Vtx (G)$
4	3 1	eqtr4di	$⊢ g = G \to Vtx (g) = V$
5	2 4	eqeq12d	$⊢ g = G \to (UnivVtx (g) = Vtx (g) \leftrightarrow UnivVtx (G) = V)$
6		df-cplgr	$⊢ ComplGraph = \{g \| UnivVtx (g) = Vtx (g)\}$
7	5 6	elab2g	$⊢ G \in W \to (G \in ComplGraph \leftrightarrow UnivVtx (G) = V)$