Theorem f1eq2 6726

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 6641	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6497	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6497	. 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 5623  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489

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 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495  df-f 6496  df-f1 6497

This theorem is referenced by:  f1co  6741  f1oeq2  6763  f1eq123d  6766  f10d  6808  brdom2g  8894  marypha1lem  9336  fseqenlem1  9934  dfac12lem2  10055  dfac12lem3  10056  ackbij2  10152  iundom2g  10450  hashf1  14380  istrkg3ld  28533  ausgrusgrb  29238  usgr0  29316  uspgr1e  29317  usgrres  29381  usgrexilem  29513  usgr2pthlem  29836  usgr2pth  29837  s2f1  33027  ccatf1  33031  cshf1o  33044  cycpmconjv  33224  cyc3evpm  33232  lindflbs  33460  matunitlindflem2  37818  eldioph2lem2  43003  f1cof1b  47323  fundcmpsurinj  47655  fundcmpsurbijinj  47656  fargshiftf1  47687  upgrimtrlslem2  48151  f102g  49097  f1mo  49098  aacllem  50046