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	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	isnat3.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	natfn2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
	nateq.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 𝑁 𝐺 ) )
Assertion	nateq	⊢ ( 𝜑 → ( 𝐴 = 𝐿 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( 𝐿 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnat3.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2		isnat3.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		natfn2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
4		nateq.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 𝑁 𝐺 ) )
5	1 2 3	natfn2	⊢ ( 𝜑 → 𝐴 Fn 𝐵 )
6	1 2 4	natfn2	⊢ ( 𝜑 → 𝐿 Fn 𝐵 )
7		eqfnfv	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐿 Fn 𝐵 ) → ( 𝐴 = 𝐿 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( 𝐿 ‘ 𝑥 ) ) )
8	5 6 7	syl2anc	⊢ ( 𝜑 → ( 𝐴 = 𝐿 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ( 𝐿 ‘ 𝑥 ) ) )