Theorem dftermc3

Description: Alternate definition of TermCat . See also df-termc , dftermc2 . (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Assertion	dftermc3	|- TermCat = { c | ( Arrow ` c ) ~~ 1o }

Proof

Step	Hyp	Ref	Expression
1		termcarweu	|- ( c e. TermCat -> E! a a e. ( Arrow ` c ) )
2		arweutermc	|- ( E! a a e. ( Arrow ` c ) -> c e. TermCat )
3	1 2	impbii	|- ( c e. TermCat <-> E! a a e. ( Arrow ` c ) )
4		euen1b	|- ( ( Arrow ` c ) ~~ 1o <-> E! a a e. ( Arrow ` c ) )
5	3 4	bitr4i	|- ( c e. TermCat <-> ( Arrow ` c ) ~~ 1o )
6	5	eqabi	|- TermCat = { c | ( Arrow ` c ) ~~ 1o }