Theorem f1eq2 6755

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 6670	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6519	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6519	. 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 5640  Fun wfun 6508  ⟶wf 6510  –1-1→wf1 6511

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fn 6517  df-f 6518  df-f1 6519

This theorem is referenced by:  f1co  6770  f1oeq2  6792  f1eq123d  6795  f10d  6837  brdom2g  8932  marypha1lem  9391  fseqenlem1  9984  dfac12lem2  10105  dfac12lem3  10106  ackbij2  10202  iundom2g  10500  hashf1  14429  istrkg3ld  28395  ausgrusgrb  29099  usgr0  29177  uspgr1e  29178  usgrres  29242  usgrexilem  29374  usgr2pthlem  29700  usgr2pth  29701  s2f1  32873  ccatf1  32877  cshf1o  32891  cycpmconjv  33106  cyc3evpm  33114  lindflbs  33357  matunitlindflem2  37618  eldioph2lem2  42756  f1cof1b  47082  fundcmpsurinj  47414  fundcmpsurbijinj  47415  fargshiftf1  47446  upgrimtrlslem2  47909  f102g  48844  f1mo  48845  aacllem  49794