Theorem f1eq2 6756

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560  ^◡ccnv 5646  Fun wfun 6515  ⟶wf 6517  –1-1→wf1 6518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-fn 6524  df-f 6525  df-f1 6526

This theorem is referenced by:  f1co  6773  f1oeq2  6795  f1eq123d  6798  f10d  6841  brdom2g  8938  marypha1lem  9379  fseqenlem1  9980  dfac12lem2  10101  dfac12lem3  10102  ackbij2  10198  iundom2g  10497  hashf1  14470  istrkg3ld  28627  ausgrusgrb  29363  usgr0  29441  uspgr1e  29442  usgrres  29506  usgrexilem  29638  usgr2pthlem  29960  usgr2pth  29961  s2f1  33120  ccatf1  33124  cshf1o  33137  cycpmconjv  33319  cyc3evpm  33327  lindflbs  33562  matunitlindflem2  38113  eldioph2lem2  43339  f1cof1b  47668  fundcmpsurinj  48012  fundcmpsurbijinj  48013  fargshiftf1  48044  upgrimtrlslem2  48524  f102g  49470  f1mo  49471  aacllem  50419