Theorem dftermc2

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

	Ref	Expression
Assertion	dftermc2	Could not format assertion : No typesetting found for |- TermCat = { c | A. d e. Cat E! f f e. ( d Func c ) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termc	Could not format ( c e. TermCat <-> A. d e. Cat E! f f e. ( d Func c ) ) : No typesetting found for |- ( c e. TermCat <-> A. d e. Cat E! f f e. ( d Func c ) ) with typecode |-
2	1	eqabi	Could not format TermCat = { c | A. d e. Cat E! f f e. ( d Func c ) } : No typesetting found for |- TermCat = { c | A. d e. Cat E! f f e. ( d Func c ) } with typecode |-