Theorem f1eq2 6800

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536  ^◡ccnv 5687  Fun wfun 6556  ⟶wf 6558  –1-1→wf1 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-fn 6565  df-f 6566  df-f1 6567

This theorem is referenced by:  f1co  6815  f1oeq2  6837  f1eq123d  6840  f10d  6882  brdom2g  8994  brdomgOLD  8996  marypha1lem  9470  fseqenlem1  10061  dfac12lem2  10182  dfac12lem3  10183  ackbij2  10279  iundom2g  10577  hashf1  14492  istrkg3ld  28483  ausgrusgrb  29196  usgr0  29274  uspgr1e  29275  usgrres  29339  usgrexilem  29471  usgr2pthlem  29795  usgr2pth  29796  s2f1  32913  ccatf1  32917  cshf1o  32931  cycpmconjv  33144  cyc3evpm  33152  lindflbs  33386  matunitlindflem2  37603  eldioph2lem2  42748  f1cof1b  47026  fundcmpsurinj  47333  fundcmpsurbijinj  47334  fargshiftf1  47365  f102g  48681  f1mo  48682  aacllem  49031