This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑐 ) }