Theorem f1eq2 6010

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ^◡ccnv 5037  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807  df-f 5808  df-f1 5809

This theorem is referenced by:  f1oeq2  6041  f1eq123d  6044  f10d  6082  brdomg  7851  marypha1lem  8222  fseqenlem1  8730  dfac12lem2  8849  dfac12lem3  8850  ackbij2  8948  iundom2g  9241  hashf1  13098  istrkg3ld  25160  isuslgra  25872  isusgra  25873  ausisusgra  25884  uslgra1  25901  usgra1  25902  cusgraexilem2  25996  2trllemE  26083  constr1trl  26118  fargshiftf1  26165  usgrcyclnl2  26169  4cycl4dv  26195  matunitlindflem2  32576  eldioph2lem2  36342  ausgrusgrb  40395  usgr0  40469  uspgr1e  40470  usgrexi  40661  usgr2pthlem  40969  usgr2pth  40970  aacllem  42356