Theorem f1eq2 6780

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ^◡ccnv 5674  Fun wfun 6534  ⟶wf 6536  –1-1→wf1 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6543  df-f 6544  df-f1 6545

This theorem is referenced by:  f1co  6796  f1oeq2  6819  f1eq123d  6822  f10d  6864  brdom2g  8947  brdomgOLD  8949  marypha1lem  9424  fseqenlem1  10015  dfac12lem2  10135  dfac12lem3  10136  ackbij2  10234  iundom2g  10531  hashf1  14414  istrkg3ld  27701  ausgrusgrb  28414  usgr0  28489  uspgr1e  28490  usgrres  28554  usgrexilem  28686  usgr2pthlem  29009  usgr2pth  29010  s2f1  32098  ccatf1  32102  cshf1o  32113  cycpmconjv  32288  cyc3evpm  32296  lindflbs  32483  matunitlindflem2  36473  eldioph2lem2  41484  f1cof1b  45771  fundcmpsurinj  46063  fundcmpsurbijinj  46064  fargshiftf1  46095  f102g  47471  f1mo  47472  aacllem  47801