Theorem f1eq2 6570

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

Assertion

Ref	Expression
f1eq2	⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))

Proof of Theorem f1eq2

Step	Hyp	Ref	Expression
1		feq2 6495	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6359	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6359	. 2 ⊢ (𝐹:𝐵–1-1→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹))
5	2, 3, 4	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533  ^◡ccnv 5553  Fun wfun 6348  ⟶wf 6350  –1-1→wf1 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-fn 6357  df-f 6358  df-f1 6359

This theorem is referenced by:  f1oeq2  6604  f1eq123d  6607  f10d  6647  brdomg  8518  marypha1lem  8896  fseqenlem1  9449  dfac12lem2  9569  dfac12lem3  9570  ackbij2  9664  iundom2g  9961  hashf1  13814  istrkg3ld  26246  ausgrusgrb  26949  usgr0  27024  uspgr1e  27025  usgrres  27089  usgrexilem  27221  usgr2pthlem  27543  usgr2pth  27544  s2f1  30621  ccatf1  30625  cshf1o  30636  cycpmconjv  30784  cyc3evpm  30792  lindflbs  30940  matunitlindflem2  34888  eldioph2lem2  39356  fundcmpsurinj  43568  fundcmpsurbijinj  43569  fargshiftf1  43600  aacllem  44901