Theorem f1eq2 6666

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ^◡ccnv 5588  Fun wfun 6427  ⟶wf 6429  –1-1→wf1 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fn 6436  df-f 6437  df-f1 6438

This theorem is referenced by:  f1co  6682  f1oeq2  6705  f1eq123d  6708  f10d  6750  brdom2g  8745  brdomgOLD  8747  marypha1lem  9192  fseqenlem1  9780  dfac12lem2  9900  dfac12lem3  9901  ackbij2  9999  iundom2g  10296  hashf1  14171  istrkg3ld  26822  ausgrusgrb  27535  usgr0  27610  uspgr1e  27611  usgrres  27675  usgrexilem  27807  usgr2pthlem  28131  usgr2pth  28132  s2f1  31219  ccatf1  31223  cshf1o  31234  cycpmconjv  31409  cyc3evpm  31417  lindflbs  31574  matunitlindflem2  35774  eldioph2lem2  40583  f1cof1b  44569  fundcmpsurinj  44861  fundcmpsurbijinj  44862  fargshiftf1  44893  f102g  46179  f1mo  46180  aacllem  46505