Theorem f1eq2 6804

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 6718	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6571	. 2 ⊢ (𝐹:𝐴⟶1-1𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6571	. 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 5657  Fun wfun 6560  ⟶wf 6562  ⟶1-1wf1 6563

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6569  df-f 6570  df-f1 6571

This theorem is used by:  f1co  6821  f1oeq2  6843  f1eq123d  6846  f10d  6890  brdom2g  9022  marypha1lem  9462  fseqenlem1  10142  dfac12lem2  10262  dfac12lem3  10263  ackbij2  10359  iundom2g  10663  hashf1  14643  ccatf1  14777  matunitlindflem2  23050  istrkg3ld  28980  ausgrusgrb  29803  usgr0  29881  uspgr1e  29882  usgrres  29946  usgrexilem  30078  usgr2pthlem  30406  usgr2pth  30407  s2f1  33606  cshf1o  33619  cycpmconjv  33802  cyc3evpm  33810  lindflbs  34038  eldioph2lem2  44038  f1cof1b  48420  fundcmpsurinj  48764  fundcmpsurbijinj  48765  fargshiftf1  48796  upgrimtrlslem2  49276  f102g  50294  f1mo  50295  aacllem  51367