Theorem f1eq2 6724

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ^◡ccnv 5621  Fun wfun 6484  ⟶wf 6486  –1-1→wf1 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-fn 6493  df-f 6494  df-f1 6495

This theorem is referenced by:  f1co  6739  f1oeq2  6761  f1eq123d  6764  f10d  6806  brdom2g  8892  marypha1lem  9334  fseqenlem1  9932  dfac12lem2  10053  dfac12lem3  10054  ackbij2  10150  iundom2g  10448  hashf1  14378  istrkg3ld  28482  ausgrusgrb  29187  usgr0  29265  uspgr1e  29266  usgrres  29330  usgrexilem  29462  usgr2pthlem  29785  usgr2pth  29786  s2f1  32976  ccatf1  32980  cshf1o  32993  cycpmconjv  33173  cyc3evpm  33181  lindflbs  33409  matunitlindflem2  37757  eldioph2lem2  42945  f1cof1b  47265  fundcmpsurinj  47597  fundcmpsurbijinj  47598  fargshiftf1  47629  upgrimtrlslem2  48093  f102g  49039  f1mo  49040  aacllem  49988