Theorem dftermc3

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

	Ref	Expression
Assertion	dftermc3	⊢ TermCat = { 𝑐 ∣ ( Arrow ‘ 𝑐 ) ≈ 1o }

Proof

Step	Hyp	Ref	Expression
1		termcarweu	⊢ ( 𝑐 ∈ TermCat → ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝑐 ) )
2		arweutermc	⊢ ( ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝑐 ) → 𝑐 ∈ TermCat )
3	1 2	impbii	⊢ ( 𝑐 ∈ TermCat ↔ ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝑐 ) )
4		euen1b	⊢ ( ( Arrow ‘ 𝑐 ) ≈ 1o ↔ ∃! 𝑎 𝑎 ∈ ( Arrow ‘ 𝑐 ) )
5	3 4	bitr4i	⊢ ( 𝑐 ∈ TermCat ↔ ( Arrow ‘ 𝑐 ) ≈ 1o )
6	5	eqabi	⊢ TermCat = { 𝑐 ∣ ( Arrow ‘ 𝑐 ) ≈ 1o }