Theorem dftermc2

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

	Ref	Expression
Assertion	dftermc2	⊢ TermCat = { 𝑐 ∣ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝑐 ) }

Proof

Step	Hyp	Ref	Expression
1		termc	⊢ ( 𝑐 ∈ TermCat ↔ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝑐 ) )
2	1	eqabi	⊢ TermCat = { 𝑐 ∣ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝑐 ) }