Theorem f1eq2 6779

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 6693	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6548	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6548	. 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 1569  ^◡ccnv 5650  Fun wfun 6537  ⟶wf 6539  –1-1→wf1 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6546  df-f 6547  df-f1 6548

This theorem is used by:  f1co  6796  f1oeq2  6818  f1eq123d  6821  f10d  6864  brdom2g  8991  marypha1lem  9432  fseqenlem1  10110  dfac12lem2  10230  dfac12lem3  10231  ackbij2  10327  iundom2g  10631  hashf1  14609  ccatf1  14743  matunitlindflem2  23004  istrkg3ld  28932  ausgrusgrb  29755  usgr0  29833  uspgr1e  29834  usgrres  29898  usgrexilem  30030  usgr2pthlem  30358  usgr2pth  30359  s2f1  33560  cshf1o  33573  cycpmconjv  33753  cyc3evpm  33761  lindflbs  33984  eldioph2lem2  43881  f1cof1b  48255  fundcmpsurinj  48599  fundcmpsurbijinj  48600  fargshiftf1  48631  upgrimtrlslem2  49111  f102g  50071  f1mo  50072  aacllem  51122