This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gropeld

Description: If any representation of a graph with vertices V and edges E is an element of an arbitrary class C , then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E ) is an element of this class C . (Contributed by AV, 11-Oct-2020)

	Ref	Expression
Hypotheses	gropeld.g	$⊢ φ \to \forall g ((Vtx (g) = V \land iEdg (g) = E) \to g \in C)$
	gropeld.v	$⊢ φ \to V \in U$
	gropeld.e	$⊢ φ \to E \in W$
Assertion	gropeld	$⊢ φ \to ⟨V, E⟩ \in C$

Proof

Step	Hyp	Ref	Expression
1		gropeld.g	$⊢ φ \to \forall g ((Vtx (g) = V \land iEdg (g) = E) \to g \in C)$
2		gropeld.v	$⊢ φ \to V \in U$
3		gropeld.e	$⊢ φ \to E \in W$
4	1 2 3	gropd	$⊢ φ \to \underset{˙}{[} ⟨V, E⟩ / g \underset{˙}{]} g \in C$
5		sbcel1v	$⊢ \underset{˙}{[} ⟨V, E⟩ / g \underset{˙}{]} g \in C \leftrightarrow ⟨V, E⟩ \in C$
6	4 5	sylib	$⊢ φ \to ⟨V, E⟩ \in C$