Theorem f1eq2 6780

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539  ^◡ccnv 5664  Fun wfun 6535  ⟶wf 6537  –1-1→wf1 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-fn 6544  df-f 6545  df-f1 6546

This theorem is referenced by:  f1co  6795  f1oeq2  6817  f1eq123d  6820  f10d  6862  brdom2g  8978  brdomgOLD  8980  marypha1lem  9455  fseqenlem1  10046  dfac12lem2  10167  dfac12lem3  10168  ackbij2  10264  iundom2g  10562  hashf1  14478  istrkg3ld  28405  ausgrusgrb  29110  usgr0  29188  uspgr1e  29189  usgrres  29253  usgrexilem  29385  usgr2pthlem  29711  usgr2pth  29712  s2f1  32869  ccatf1  32873  cshf1o  32887  cycpmconjv  33101  cyc3evpm  33109  lindflbs  33342  matunitlindflem2  37583  eldioph2lem2  42735  f1cof1b  47047  fundcmpsurinj  47354  fundcmpsurbijinj  47355  fargshiftf1  47386  f102g  48719  f1mo  48720  aacllem  49328