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	$$⊢\mathrm{AcyclicGraph}=\left\{g|\forall f\forall p\left(f\mathrm{Cycles}\left(g\right)p\to f=\varnothing \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-acycgr	$$⊢\mathrm{AcyclicGraph}=\left\{g|\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\right\}$$
2		2exanali	$$⊢\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge \neg f=\varnothing \right)\leftrightarrow \forall f\forall p\left(f\mathrm{Cycles}\left(g\right)p\to f=\varnothing \right)$$
3		df-ne	$$⊢f\ne \varnothing \leftrightarrow \neg f=\varnothing$$
4	3	anbi2i	$$⊢\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\leftrightarrow \left(f\mathrm{Cycles}\left(g\right)p\wedge \neg f=\varnothing \right)$$
5	4	2exbii	$$⊢\exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\leftrightarrow \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge \neg f=\varnothing \right)$$
6	2 5	xchnxbir	$$⊢\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\leftrightarrow \forall f\forall p\left(f\mathrm{Cycles}\left(g\right)p\to f=\varnothing \right)$$
7	6	abbii	$$⊢\left\{g|\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\right\}=\left\{g|\forall f\forall p\left(f\mathrm{Cycles}\left(g\right)p\to f=\varnothing \right)\right\}$$
8	1 7	eqtri	$$⊢\mathrm{AcyclicGraph}=\left\{g|\forall f\forall p\left(f\mathrm{Cycles}\left(g\right)p\to f=\varnothing \right)\right\}$$