Theorem f1eq2 6734

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 6649	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6504	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6504	. 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 5630  Fun wfun 6493  ⟶wf 6495  –1-1→wf1 6496

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 6502  df-f 6503  df-f1 6504

This theorem is referenced by:  f1co  6749  f1oeq2  6771  f1eq123d  6774  f10d  6816  brdom2g  8906  marypha1lem  9360  fseqenlem1  9953  dfac12lem2  10074  dfac12lem3  10075  ackbij2  10171  iundom2g  10469  hashf1  14398  istrkg3ld  28441  ausgrusgrb  29145  usgr0  29223  uspgr1e  29224  usgrres  29288  usgrexilem  29420  usgr2pthlem  29743  usgr2pth  29744  s2f1  32916  ccatf1  32920  cshf1o  32934  cycpmconjv  33114  cyc3evpm  33122  lindflbs  33343  matunitlindflem2  37604  eldioph2lem2  42742  f1cof1b  47071  fundcmpsurinj  47403  fundcmpsurbijinj  47404  fargshiftf1  47435  upgrimtrlslem2  47898  f102g  48833  f1mo  48834  aacllem  49783