Theorem f1oeq3dd

Description: Equality deduction for one-to-one onto functions. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	f1oeq3dd.1	|- ( ph -> F : C -1-1-onto-> A )
	f1oeq3dd.2	|- ( ph -> A = B )
Assertion	f1oeq3dd	|- ( ph -> F : C -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		f1oeq3dd.1	|- ( ph -> F : C -1-1-onto-> A )
2		f1oeq3dd.2	|- ( ph -> A = B )
3	2	f1oeq3d	|- ( ph -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )
4	1 3	mpbid	|- ( ph -> F : C -1-1-onto-> B )