Theorem f1eq2 6813

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ^◡ccnv 5699  Fun wfun 6567  ⟶wf 6569  –1-1→wf1 6570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576  df-f 6577  df-f1 6578

This theorem is referenced by:  f1co  6828  f1oeq2  6851  f1eq123d  6854  f10d  6896  brdom2g  9015  brdomgOLD  9017  marypha1lem  9502  fseqenlem1  10093  dfac12lem2  10214  dfac12lem3  10215  ackbij2  10311  iundom2g  10609  hashf1  14506  istrkg3ld  28487  ausgrusgrb  29200  usgr0  29278  uspgr1e  29279  usgrres  29343  usgrexilem  29475  usgr2pthlem  29799  usgr2pth  29800  s2f1  32911  ccatf1  32915  cshf1o  32929  cycpmconjv  33135  cyc3evpm  33143  lindflbs  33372  matunitlindflem2  37577  eldioph2lem2  42717  f1cof1b  46992  fundcmpsurinj  47283  fundcmpsurbijinj  47284  fargshiftf1  47315  f102g  48565  f1mo  48566  aacllem  48895