Theorem f1eq2 6715

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ^◡ccnv 5613  Fun wfun 6475  ⟶wf 6477  –1-1→wf1 6478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484  df-f 6485  df-f1 6486

This theorem is referenced by:  f1co  6730  f1oeq2  6752  f1eq123d  6755  f10d  6797  brdom2g  8880  marypha1lem  9317  fseqenlem1  9915  dfac12lem2  10036  dfac12lem3  10037  ackbij2  10133  iundom2g  10431  hashf1  14364  istrkg3ld  28439  ausgrusgrb  29143  usgr0  29221  uspgr1e  29222  usgrres  29286  usgrexilem  29418  usgr2pthlem  29741  usgr2pth  29742  s2f1  32926  ccatf1  32930  cshf1o  32943  cycpmconjv  33111  cyc3evpm  33119  lindflbs  33344  matunitlindflem2  37665  eldioph2lem2  42802  f1cof1b  47116  fundcmpsurinj  47448  fundcmpsurbijinj  47449  fargshiftf1  47480  upgrimtrlslem2  47944  f102g  48891  f1mo  48892  aacllem  49841