Metamath Proof Explorer

Theorem dftermc2

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

Ref Expression
Assertion dftermc2 
|- TermCat = { c | A. d e. Cat E! f f e. ( d Func c ) }

Proof

Step Hyp Ref Expression
1 termc 
 |-  ( c e. TermCat <-> A. d e. Cat E! f f e. ( d Func c ) )
2 1 eqabi 
 |-  TermCat = { c | A. d e. Cat E! f f e. ( d Func c ) }