Theorem f1eq2 6650

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ^◡ccnv 5579  Fun wfun 6412  ⟶wf 6414  –1-1→wf1 6415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421  df-f 6422  df-f1 6423

This theorem is referenced by:  f1co  6666  f1oeq2  6689  f1eq123d  6692  f10d  6733  brdomg  8703  marypha1lem  9122  fseqenlem1  9711  dfac12lem2  9831  dfac12lem3  9832  ackbij2  9930  iundom2g  10227  hashf1  14099  istrkg3ld  26726  ausgrusgrb  27438  usgr0  27513  uspgr1e  27514  usgrres  27578  usgrexilem  27710  usgr2pthlem  28032  usgr2pth  28033  s2f1  31121  ccatf1  31125  cshf1o  31136  cycpmconjv  31311  cyc3evpm  31319  lindflbs  31476  matunitlindflem2  35701  eldioph2lem2  40499  f1cof1b  44456  fundcmpsurinj  44749  fundcmpsurbijinj  44750  fargshiftf1  44781  f102g  46067  f1mo  46068  aacllem  46391