Metamath Proof Explorer


Theorem gropd

Description: If any representation of a graph with vertices V and edges E has a certain property ps , 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 ) has this property. (Contributed by AV, 11-Oct-2020)

Ref Expression
Hypotheses gropd.g
|- ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) )
gropd.v
|- ( ph -> V e. U )
gropd.e
|- ( ph -> E e. W )
Assertion gropd
|- ( ph -> [. <. V , E >. / g ]. ps )

Proof

Step Hyp Ref Expression
1 gropd.g
 |-  ( ph -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) )
2 gropd.v
 |-  ( ph -> V e. U )
3 gropd.e
 |-  ( ph -> E e. W )
4 opex
 |-  <. V , E >. e. _V
5 4 a1i
 |-  ( ph -> <. V , E >. e. _V )
6 opvtxfv
 |-  ( ( V e. U /\ E e. W ) -> ( Vtx ` <. V , E >. ) = V )
7 opiedgfv
 |-  ( ( V e. U /\ E e. W ) -> ( iEdg ` <. V , E >. ) = E )
8 6 7 jca
 |-  ( ( V e. U /\ E e. W ) -> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) )
9 2 3 8 syl2anc
 |-  ( ph -> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) )
10 nfcv
 |-  F/_ g <. V , E >.
11 nfv
 |-  F/ g ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E )
12 nfsbc1v
 |-  F/ g [. <. V , E >. / g ]. ps
13 11 12 nfim
 |-  F/ g ( ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) -> [. <. V , E >. / g ]. ps )
14 fveqeq2
 |-  ( g = <. V , E >. -> ( ( Vtx ` g ) = V <-> ( Vtx ` <. V , E >. ) = V ) )
15 fveqeq2
 |-  ( g = <. V , E >. -> ( ( iEdg ` g ) = E <-> ( iEdg ` <. V , E >. ) = E ) )
16 14 15 anbi12d
 |-  ( g = <. V , E >. -> ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) <-> ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) ) )
17 sbceq1a
 |-  ( g = <. V , E >. -> ( ps <-> [. <. V , E >. / g ]. ps ) )
18 16 17 imbi12d
 |-  ( g = <. V , E >. -> ( ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) <-> ( ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) -> [. <. V , E >. / g ]. ps ) ) )
19 10 13 18 spcgf
 |-  ( <. V , E >. e. _V -> ( A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = E ) -> ps ) -> ( ( ( Vtx ` <. V , E >. ) = V /\ ( iEdg ` <. V , E >. ) = E ) -> [. <. V , E >. / g ]. ps ) ) )
20 5 1 9 19 syl3c
 |-  ( ph -> [. <. V , E >. / g ]. ps )