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	|- ( ph -> A e. ( F N G ) )
	nateq.l	|- ( ph -> L e. ( F N G ) )
Assertion	nateq	|- ( ph -> ( A = L <-> A. x e. 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	|- ( ph -> A e. ( F N G ) )
4		nateq.l	|- ( ph -> L e. ( F N G ) )
5	1 2 3	natfn2	|- ( ph -> A Fn B )
6	1 2 4	natfn2	|- ( ph -> L Fn B )
7		eqfnfv	|- ( ( A Fn B /\ L Fn B ) -> ( A = L <-> A. x e. B ( A ` x ) = ( L ` x ) ) )
8	5 6 7	syl2anc	|- ( ph -> ( A = L <-> A. x e. B ( A ` x ) = ( L ` x ) ) )