Theorem f1oeq3dd

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

	Ref	Expression
Hypotheses	f1oeq3dd.1	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}A$$
	f1oeq3dd.2	$$⊢\phi \to A=B$$
Assertion	f1oeq3dd	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		f1oeq3dd.1	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}A$$
2		f1oeq3dd.2	$$⊢\phi \to A=B$$
3	2	f1oeq3d	$$⊢\phi \to \left(F:C\underset{1-1\; onto}{⟶}A\leftrightarrow F:C\underset{1-1\; onto}{⟶}B\right)$$
4	1 3	mpbid	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}B$$