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 \in USHGraph \to G \in UHGraph$

Step	Hyp	Ref	Expression
1		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
2		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
3	1 2	syl	$⊢ G \in USHGraph \to G \in UHGraph$