Metamath Proof Explorer


Theorem crcts

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

Ref Expression
Assertion crcts Circuits G = f p | f Trails 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-crcts Circuits = g V f p | f Trails g p p 0 = p f
3 1 2 fvmptopab Circuits G = f p | f Trails G p p 0 = p f