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 φ g Vtx g = V iEdg g = E ψ
gropd.v φ V U
gropd.e φ E W
Assertion gropd φ [˙ V E / g]˙ ψ

Proof

Step Hyp Ref Expression
1 gropd.g φ g Vtx g = V iEdg g = E ψ
2 gropd.v φ V U
3 gropd.e φ E W
4 opex V E V
5 4 a1i φ V E V
6 opvtxfv V U E W Vtx V E = V
7 opiedgfv V U E W iEdg V E = E
8 6 7 jca V U E W Vtx V E = V iEdg V E = E
9 2 3 8 syl2anc φ Vtx V E = V iEdg V E = E
10 nfcv _ g V E
11 nfv g Vtx V E = V iEdg V E = E
12 nfsbc1v g [˙ V E / g]˙ ψ
13 11 12 nfim g Vtx V E = V iEdg V E = E [˙ V E / g]˙ ψ
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 ψ [˙ V E / g]˙ ψ
18 16 17 imbi12d g = V E Vtx g = V iEdg g = E ψ Vtx V E = V iEdg V E = E [˙ V E / g]˙ ψ
19 10 13 18 spcgf V E V g Vtx g = V iEdg g = E ψ Vtx V E = V iEdg V E = E [˙ V E / g]˙ ψ
20 5 1 9 19 syl3c φ [˙ V E / g]˙ ψ