Theorem f1eq2 6774

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ^◡ccnv 5662  Fun wfun 6534  ⟶wf 6536  –1-1→wf1 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-fn 6543  df-f 6544  df-f1 6545

This theorem is used by:  f1co  6791  f1oeq2  6813  f1eq123d  6816  f10d  6859  brdom2g  8960  marypha1lem  9400  fseqenlem1  10024  dfac12lem2  10144  dfac12lem3  10145  ackbij2  10241  iundom2g  10539  hashf1  14512  ccatf1  14646  istrkg3ld  28781  ausgrusgrb  29573  usgr0  29651  uspgr1e  29652  usgrres  29716  usgrexilem  29848  usgr2pthlem  30176  usgr2pth  30177  s2f1  33333  cshf1o  33346  cycpmconjv  33526  cyc3evpm  33534  lindflbs  33756  matunitlindflem2  38325  eldioph2lem2  43550  f1cof1b  47872  fundcmpsurinj  48216  fundcmpsurbijinj  48217  fargshiftf1  48248  upgrimtrlslem2  48728  f102g  49687  f1mo  49688  aacllem  50678