Metamath Proof Explorer

Theorem isomgrsymb

Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022)

		Ref	Expression
	Assertion	isomgrsymb	$⊢ (A \in UHGraph \land B \in UHGraph) \to (A IsomGr B \leftrightarrow B IsomGr A)$

Step	Hyp	Ref	Expression
1		isomgrsym	$⊢ (A \in UHGraph \land B \in UHGraph) \to (A IsomGr B \to B IsomGr A)$
2		isomgrsym	$⊢ (B \in UHGraph \land A \in UHGraph) \to (B IsomGr A \to A IsomGr B)$
3	2	ancoms	$⊢ (A \in UHGraph \land B \in UHGraph) \to (B IsomGr A \to A IsomGr B)$
4	1 3	impbid	$⊢ (A \in UHGraph \land B \in UHGraph) \to (A IsomGr B \leftrightarrow B IsomGr A)$