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	|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> g e. C ) )
	gropeld.v	|- ( ph -> V e. U )
	gropeld.e	|- ( ph -> E e. W )
Assertion	gropeld	|- ( ph -> <. V , E >. e. C )

Proof

Step	Hyp	Ref	Expression
1		gropeld.g	|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> g e. C ) )
2		gropeld.v	|- ( ph -> V e. U )
3		gropeld.e	|- ( ph -> E e. W )
4	1 2 3	gropd	|- ( ph -> [. <. V , E >. / g ]. g e. C )
5		sbcel1v	|- ( [. <. V , E >. / g ]. g e. C <-> <. V , E >. e. C )
6	4 5	sylib	|- ( ph -> <. V , E >. e. C )