Metamath Proof Explorer

Theorem frgr0

Description: The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021)

Ref Expression
Assertion frgr0 
|- (/) e. FriendGraph

Proof

Step Hyp Ref Expression
1 usgr0 
 |-  (/) e. USGraph
2 ral0 
 |-  A. k e. (/) A. l e. ( (/) \ { k } ) E! x e. (/) { { x , k } , { x , l } } C_ ( Edg ` (/) )
3 vtxval0 
 |-  ( Vtx ` (/) ) = (/)
4 3 eqcomi 
 |-  (/) = ( Vtx ` (/) )
5 eqid 
 |-  ( Edg ` (/) ) = ( Edg ` (/) )
6 4 5 isfrgr 
 |-  ( (/) e. FriendGraph <-> ( (/) e. USGraph /\ A. k e. (/) A. l e. ( (/) \ { k } ) E! x e. (/) { { x , k } , { x , l } } C_ ( Edg ` (/) ) ) )
7 1 2 6 mpbir2an 
 |-  (/) e. FriendGraph