Theorem f1eq2 6770

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ^◡ccnv 5653  Fun wfun 6525  ⟶wf 6527  –1-1→wf1 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-fn 6534  df-f 6535  df-f1 6536

This theorem is referenced by:  f1co  6785  f1oeq2  6807  f1eq123d  6810  f10d  6852  brdom2g  8970  brdomgOLD  8972  marypha1lem  9445  fseqenlem1  10038  dfac12lem2  10159  dfac12lem3  10160  ackbij2  10256  iundom2g  10554  hashf1  14475  istrkg3ld  28440  ausgrusgrb  29144  usgr0  29222  uspgr1e  29223  usgrres  29287  usgrexilem  29419  usgr2pthlem  29745  usgr2pth  29746  s2f1  32920  ccatf1  32924  cshf1o  32938  cycpmconjv  33153  cyc3evpm  33161  lindflbs  33394  matunitlindflem2  37641  eldioph2lem2  42784  f1cof1b  47106  fundcmpsurinj  47423  fundcmpsurbijinj  47424  fargshiftf1  47455  upgrimtrlslem2  47918  f102g  48830  f1mo  48831  aacllem  49665