Theorem f1eq2 6258

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632  ^◡ccnv 5265  Fun wfun 6043  ⟶wf 6045  –1-1→wf1 6046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-fn 6052  df-f 6053  df-f1 6054

This theorem is referenced by:  f1oeq2  6289  f1eq123d  6292  f10d  6331  brdomg  8131  marypha1lem  8504  fseqenlem1  9037  dfac12lem2  9158  dfac12lem3  9159  ackbij2  9257  iundom2g  9554  hashf1  13433  istrkg3ld  25559  ausgrusgrb  26259  usgr0  26334  uspgr1e  26335  usgrres  26399  usgrexilem  26546  usgr2pthlem  26869  usgr2pth  26870  matunitlindflem2  33719  eldioph2lem2  37826  fargshiftf1  41887  aacllem  43060