Metamath Proof Explorer

Theorem uspgruhgr

Description: An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025)

Ref Expression
Assertion uspgruhgr 
|- ( G e. USPGraph -> G e. UHGraph )

Proof

Step Hyp Ref Expression
1 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
2 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
3 1 2 syl 
 |-  ( G e. USPGraph -> G e. UHGraph )