Theorem f1eq2 6573

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ^◡ccnv 5556  Fun wfun 6351  ⟶wf 6353  –1-1→wf1 6354

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-fn 6360  df-f 6361  df-f1 6362

This theorem is referenced by:  f1oeq2  6607  f1eq123d  6610  f10d  6650  brdomg  8521  marypha1lem  8899  fseqenlem1  9452  dfac12lem2  9572  dfac12lem3  9573  ackbij2  9667  iundom2g  9964  hashf1  13818  istrkg3ld  26249  ausgrusgrb  26952  usgr0  27027  uspgr1e  27028  usgrres  27092  usgrexilem  27224  usgr2pthlem  27546  usgr2pth  27547  s2f1  30623  ccatf1  30627  cshf1o  30638  cycpmconjv  30786  cyc3evpm  30794  lindflbs  30942  matunitlindflem2  34891  eldioph2lem2  39365  fundcmpsurinj  43576  fundcmpsurbijinj  43577  fargshiftf1  43608  aacllem  44909