Metamath Proof Explorer

Theorem frgruhgr0v

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

Ref Expression
Assertion frgruhgr0v 
|- ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. FriendGraph )

Proof

Step Hyp Ref Expression
1 uhgr0vb 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )
2 1 biimpcd 
 |-  ( G e. UHGraph -> ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( iEdg ` G ) = (/) ) )
3 2 anabsi5 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
4 frgr0vb 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) /\ ( iEdg ` G ) = (/) ) -> G e. FriendGraph )
5 3 4 mpd3an3 
 |-  ( ( G e. UHGraph /\ ( Vtx ` G ) = (/) ) -> G e. FriendGraph )