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 e. W -> ( G e. 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 e. W -> ( G e. ComplGraph <-> ( UnivVtx ` G ) = V ) )