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 ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ FriendGraph

Proof

Step Hyp Ref Expression
1 uhgr0vb ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ UHGraph ↔ iEdg ⁡ G = ∅
2 1 biimpcd ⊢ G ∈ UHGraph → G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → iEdg ⁡ G = ∅
3 2 anabsi5 ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → iEdg ⁡ G = ∅
4 frgr0vb ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ FriendGraph
5 3 4 mpd3an3 ⊢ G ∈ UHGraph ∧ Vtx ⁡ G = ∅ → G ∈ FriendGraph