subgrprop

	Ref	Expression
Hypotheses	issubgr.v	$⊢ V = Vtx (S)$
	issubgr.a	$⊢ A = Vtx (G)$
	issubgr.i	$⊢ I = iEdg (S)$
	issubgr.b	$⊢ B = iEdg (G)$
	issubgr.e	$⊢ E = Edg (S)$
Assertion	subgrprop	$⊢ S SubGraph G \to (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V)$

Step	Hyp	Ref	Expression
1		issubgr.v	$⊢ V = Vtx (S)$
2		issubgr.a	$⊢ A = Vtx (G)$
3		issubgr.i	$⊢ I = iEdg (S)$
4		issubgr.b	$⊢ B = iEdg (G)$
5		issubgr.e	$⊢ E = Edg (S)$
6		subgrv	$⊢ S SubGraph G \to (S \in V \land G \in V)$
7	1 2 3 4 5	issubgr	$⊢ (G \in V \land S \in V) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V))$
8	7	biimpd	$⊢ (G \in V \land S \in V) \to (S SubGraph G \to (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V))$
9	8	ancoms	$⊢ (S \in V \land G \in V) \to (S SubGraph G \to (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V))$
10	6 9	mpcom	$⊢ S SubGraph G \to (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V)$

Metamath Proof Explorer