Theorem f1eq2

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997)

	Ref	Expression
Assertion	f1eq2	$$⊢A=B\to \left(F:A\underset{1-1}{⟶}C\leftrightarrow F:B\underset{1-1}{⟶}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		feq2	$$⊢A=B\to \left(F:A⟶C\leftrightarrow F:B⟶C\right)$$
2	1	anbi1d	$$⊢A=B\to \left(\left(F:A⟶C\wedge \mathrm{Fun}{F}^{-1}\right)\leftrightarrow \left(F:B⟶C\wedge \mathrm{Fun}{F}^{-1}\right)\right)$$
3		df-f1	$$⊢F:A\underset{1-1}{⟶}C\leftrightarrow \left(F:A⟶C\wedge \mathrm{Fun}{F}^{-1}\right)$$
4		df-f1	$$⊢F:B\underset{1-1}{⟶}C\leftrightarrow \left(F:B⟶C\wedge \mathrm{Fun}{F}^{-1}\right)$$
5	2 3 4	3bitr4g	$$⊢A=B\to \left(F:A\underset{1-1}{⟶}C\leftrightarrow F:B\underset{1-1}{⟶}C\right)$$