Metamath Proof Explorer


Theorem cycls

Description: The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021)

Ref Expression
Assertion cycls Cycles G = f p | f Paths G p p 0 = p f

Proof

Step Hyp Ref Expression
1 biidd g = G p 0 = p f p 0 = p f
2 df-cycls Cycles = g V f p | f Paths g p p 0 = p f
3 1 2 fvmptopab Cycles G = f p | f Paths G p p 0 = p f