Theorem f1eq2 6312

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   = wceq 1653  ^◡ccnv 5311  Fun wfun 6095  ⟶wf 6097  –1-1→wf1 6098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2792  df-fn 6104  df-f 6105  df-f1 6106

This theorem is referenced by:  f1oeq2  6346  f1eq123d  6349  f10d  6389  brdomg  8205  marypha1lem  8581  fseqenlem1  9133  dfac12lem2  9254  dfac12lem3  9255  ackbij2  9353  iundom2g  9650  hashf1  13490  istrkg3ld  25712  ausgrusgrb  26401  usgr0  26477  uspgr1e  26478  usgrres  26542  usgrexilem  26690  usgr2pthlem  27017  usgr2pth  27018  matunitlindflem2  33895  eldioph2lem2  38110  fargshiftf1  42217  aacllem  43349