Theorem func1st2nd

Description: Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypothesis	func1st2nd.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		func1st2nd.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
3		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
4	2 1 3	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )