Metamath Proof Explorer

Theorem frgrusgr

Description: A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Assertion frgrusgr 
|- ( G e. FriendGraph -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 isfrgr 
 |-  ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
4 3 simplbi 
 |-  ( G e. FriendGraph -> G e. USGraph )