Metamath Proof Explorer

Theorem isubgrusgr

Description: An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025)

		Ref	Expression
	Hypothesis	isubgrupgr.v	$⊢ V = Vtx (G)$
	Assertion	isubgrusgr	$⊢ (G \in USGraph \land S \subseteq V) \to G ISubGr S \in USGraph$

Step	Hyp	Ref	Expression
1		isubgrupgr.v	$⊢ V = Vtx (G)$
2		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
3	1	isubgrsubgr	$⊢ (G \in UHGraph \land S \subseteq V) \to (G ISubGr S) SubGraph G$
4	2 3	sylan	$⊢ (G \in USGraph \land S \subseteq V) \to (G ISubGr S) SubGraph G$
5		subusgr	$⊢ (G \in USGraph \land (G ISubGr S) SubGraph G) \to G ISubGr S \in USGraph$
6	4 5	syldan	$⊢ (G \in USGraph \land S \subseteq V) \to G ISubGr S \in USGraph$