Theorem f1eq2 6772

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ^◡ccnv 5650  Fun wfun 6531  ⟶wf 6533  –1-1→wf1 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6540  df-f 6541  df-f1 6542

This theorem is used by:  f1co  6789  f1oeq2  6811  f1eq123d  6814  f10d  6857  brdom2g  8977  marypha1lem  9418  fseqenlem1  10096  dfac12lem2  10216  dfac12lem3  10217  ackbij2  10313  iundom2g  10617  hashf1  14595  ccatf1  14729  matunitlindflem2  22988  istrkg3ld  28916  ausgrusgrb  29739  usgr0  29817  uspgr1e  29818  usgrres  29882  usgrexilem  30014  usgr2pthlem  30342  usgr2pth  30343  s2f1  33503  cshf1o  33516  cycpmconjv  33696  cyc3evpm  33704  lindflbs  33927  eldioph2lem2  43751  f1cof1b  48116  fundcmpsurinj  48460  fundcmpsurbijinj  48461  fargshiftf1  48492  upgrimtrlslem2  48972  f102g  49931  f1mo  49932  aacllem  50908