Theorem f1eq2 6545

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ^◡ccnv 5518  Fun wfun 6318  ⟶wf 6320  –1-1→wf1 6321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6327  df-f 6328  df-f1 6329

This theorem is referenced by:  f1oeq2  6580  f1eq123d  6583  f10d  6623  brdomg  8502  marypha1lem  8881  fseqenlem1  9435  dfac12lem2  9555  dfac12lem3  9556  ackbij2  9654  iundom2g  9951  hashf1  13811  istrkg3ld  26255  ausgrusgrb  26958  usgr0  27033  uspgr1e  27034  usgrres  27098  usgrexilem  27230  usgr2pthlem  27552  usgr2pth  27553  s2f1  30647  ccatf1  30651  cshf1o  30662  cycpmconjv  30834  cyc3evpm  30842  lindflbs  30994  matunitlindflem2  35054  eldioph2lem2  39702  fundcmpsurinj  43926  fundcmpsurbijinj  43927  fargshiftf1  43958  aacllem  45329