Metamath Proof Explorer


Theorem cplgr0

Description: The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion cplgr0 ComplGraph

Proof

Step Hyp Ref Expression
1 ral0 v v UnivVtx
2 vtxval0 Vtx =
3 2 raleqi v Vtx v UnivVtx v v UnivVtx
4 1 3 mpbir v Vtx v UnivVtx
5 0ex V
6 eqid Vtx = Vtx
7 6 iscplgr V ComplGraph v Vtx v UnivVtx
8 5 7 ax-mp ComplGraph v Vtx v UnivVtx
9 4 8 mpbir ComplGraph