Theorem f1eq2 6752

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ^◡ccnv 5637  Fun wfun 6505  ⟶wf 6507  –1-1→wf1 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514  df-f 6515  df-f1 6516

This theorem is referenced by:  f1co  6767  f1oeq2  6789  f1eq123d  6792  f10d  6834  brdom2g  8929  marypha1lem  9384  fseqenlem1  9977  dfac12lem2  10098  dfac12lem3  10099  ackbij2  10195  iundom2g  10493  hashf1  14422  istrkg3ld  28388  ausgrusgrb  29092  usgr0  29170  uspgr1e  29171  usgrres  29235  usgrexilem  29367  usgr2pthlem  29693  usgr2pth  29694  s2f1  32866  ccatf1  32870  cshf1o  32884  cycpmconjv  33099  cyc3evpm  33107  lindflbs  33350  matunitlindflem2  37611  eldioph2lem2  42749  f1cof1b  47078  fundcmpsurinj  47410  fundcmpsurbijinj  47411  fargshiftf1  47442  upgrimtrlslem2  47905  f102g  48840  f1mo  48841  aacllem  49790