Metamath Proof Explorer


Definition df-acycgr

Description: Define the class of all acyclic graphs. A graph is calledacyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023)

Ref Expression
Assertion df-acycgr AcyclicGraph = g | ¬ f p f Cycles g p f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cacycgr class AcyclicGraph
1 vg setvar g
2 vf setvar f
3 vp setvar p
4 2 cv setvar f
5 ccycls class Cycles
6 1 cv setvar g
7 6 5 cfv class Cycles g
8 3 cv setvar p
9 4 8 7 wbr wff f Cycles g p
10 c0 class
11 4 10 wne wff f
12 9 11 wa wff f Cycles g p f
13 12 3 wex wff p f Cycles g p f
14 13 2 wex wff f p f Cycles g p f
15 14 wn wff ¬ f p f Cycles g p f
16 15 1 cab class g | ¬ f p f Cycles g p f
17 0 16 wceq wff AcyclicGraph = g | ¬ f p f Cycles g p f