Metamath Proof Explorer

Theorem nateq

Description: Two natural transformations with the same source and target are equal exactly when all their components agree. (Contributed by Zhi Wang, 14-Sep-2026)

		Ref	Expression
	Hypotheses	isnat3.n	$⊢ N = C Nat D$
		isnat3.b	$⊢ B = {Base}_{C}$
		natfn2.a	$⊢ φ \to A \in (F N G)$
		nateq.l	$⊢ φ \to L \in (F N G)$
	Assertion	nateq	$⊢ φ \to (A = L \leftrightarrow \forall x \in B A (x) = L (x))$

Proof

Step	Hyp	Ref	Expression
1		isnat3.n	$⊢ N = C Nat D$
2		isnat3.b	$⊢ B = {Base}_{C}$
3		natfn2.a	$⊢ φ \to A \in (F N G)$
4		nateq.l	$⊢ φ \to L \in (F N G)$
5	1 2 3	natfn2	$⊢ φ \to A Fn B$
6	1 2 4	natfn2	$⊢ φ \to L Fn B$
7		eqfnfv	$⊢ (A Fn B \land L Fn B) \to (A = L \leftrightarrow \forall x \in B A (x) = L (x))$
8	5 6 7	syl2anc	$⊢ φ \to (A = L \leftrightarrow \forall x \in B A (x) = L (x))$