Metamath Proof Explorer


Theorem spthsfval

Description: The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion spthsfval SPaths G = f p | f Trails G p Fun p -1

Proof

Step Hyp Ref Expression
1 biidd g = G Fun p -1 Fun p -1
2 df-spths SPaths = g V f p | f Trails g p Fun p -1
3 1 2 fvmptopab SPaths G = f p | f Trails G p Fun p -1