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	$$⊢\phi \to \forall g\left(\left(\mathrm{Vtx}\left(g\right)=V\wedge \mathrm{iEdg}\left(g\right)=E\right)\to g\in C\right)$$
	gropeld.v	$$⊢\phi \to V\in U$$
	gropeld.e	$$⊢\phi \to E\in W$$
Assertion	gropeld	$$⊢\phi \to ⟨V,E⟩\in C$$

Proof

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