Theorem f1eq2 6774

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 6690	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 629	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6539	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6539	. 2 ⊢ (𝐹:𝐵–1-1→𝐶 ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533  ^◡ccnv 5666  Fun wfun 6528  ⟶wf 6530  –1-1→wf1 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-fn 6537  df-f 6538  df-f1 6539

This theorem is referenced by:  f1co  6790  f1oeq2  6813  f1eq123d  6816  f10d  6858  brdom2g  8948  brdomgOLD  8950  marypha1lem  9425  fseqenlem1  10016  dfac12lem2  10136  dfac12lem3  10137  ackbij2  10235  iundom2g  10532  hashf1  14416  istrkg3ld  28184  ausgrusgrb  28897  usgr0  28972  uspgr1e  28973  usgrres  29037  usgrexilem  29169  usgr2pthlem  29492  usgr2pth  29493  s2f1  32581  ccatf1  32585  cshf1o  32596  cycpmconjv  32772  cyc3evpm  32780  lindflbs  32967  matunitlindflem2  36979  eldioph2lem2  42013  f1cof1b  46295  fundcmpsurinj  46587  fundcmpsurbijinj  46588  fargshiftf1  46619  f102g  47730  f1mo  47731  aacllem  48060