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  28364  ausgrusgrb  29068  usgr0  29146  uspgr1e  29147  usgrres  29211  usgrexilem  29343  usgr2pthlem  29666  usgr2pth  29667  s2f1  32839  ccatf1  32843  cshf1o  32857  cycpmconjv  33072  cyc3evpm  33080  lindflbs  33323  matunitlindflem2  37584  eldioph2lem2  42722  f1cof1b  47051  fundcmpsurinj  47383  fundcmpsurbijinj  47384  fargshiftf1  47415  upgrimtrlslem2  47878  f102g  48813  f1mo  48814  aacllem  49763