Metamath Proof Explorer


Theorem dfacycgr1

Description: An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023)

Ref Expression
Assertion dfacycgr1 AcyclicGraph = g | f p f Cycles g p f =

Proof

Step Hyp Ref Expression
1 df-acycgr AcyclicGraph = g | ¬ f p f Cycles g p f
2 2exanali ¬ f p f Cycles g p ¬ f = f p f Cycles g p f =
3 df-ne f ¬ f =
4 3 anbi2i f Cycles g p f f Cycles g p ¬ f =
5 4 2exbii f p f Cycles g p f f p f Cycles g p ¬ f =
6 2 5 xchnxbir ¬ f p f Cycles g p f f p f Cycles g p f =
7 6 abbii g | ¬ f p f Cycles g p f = g | f p f Cycles g p f =
8 1 7 eqtri AcyclicGraph = g | f p f Cycles g p f =