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

Metamath Proof Explorer

Theorem func1st2nd

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

		Ref	Expression
	Hypothesis	func1st2nd.1	$⊢ φ \to F \in (C Func D)$
	Assertion	func1st2nd	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$

Step	Hyp	Ref	Expression
1		func1st2nd.1	$⊢ φ \to F \in (C Func D)$
2		relfunc	$⊢ Rel (C Func D)$
3		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
4	2 1 3	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$