Theorem f1eq2 6784

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ^◡ccnv 5676  Fun wfun 6538  ⟶wf 6540  –1-1→wf1 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547  df-f 6548  df-f1 6549

This theorem is referenced by:  f1co  6800  f1oeq2  6823  f1eq123d  6826  f10d  6868  brdom2g  8951  brdomgOLD  8953  marypha1lem  9428  fseqenlem1  10019  dfac12lem2  10139  dfac12lem3  10140  ackbij2  10238  iundom2g  10535  hashf1  14418  istrkg3ld  27712  ausgrusgrb  28425  usgr0  28500  uspgr1e  28501  usgrres  28565  usgrexilem  28697  usgr2pthlem  29020  usgr2pth  29021  s2f1  32111  ccatf1  32115  cshf1o  32126  cycpmconjv  32301  cyc3evpm  32309  lindflbs  32495  matunitlindflem2  36485  eldioph2lem2  41499  f1cof1b  45785  fundcmpsurinj  46077  fundcmpsurbijinj  46078  fargshiftf1  46109  f102g  47518  f1mo  47519  aacllem  47848