Theorem f1eq2 6771

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ^◡ccnv 5661  Fun wfun 6531  ⟶wf 6533  –1-1→wf1 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fn 6540  df-f 6541  df-f1 6542

This theorem is referenced by:  f1co  6788  f1oeq2  6810  f1eq123d  6813  f10d  6856  brdom2g  8953  marypha1lem  9392  fseqenlem1  10007  dfac12lem2  10127  dfac12lem3  10128  ackbij2  10224  iundom2g  10523  hashf1  14493  istrkg3ld  28695  ausgrusgrb  29455  usgr0  29533  uspgr1e  29534  usgrres  29598  usgrexilem  29730  usgr2pthlem  30052  usgr2pth  30053  s2f1  33205  ccatf1  33209  cshf1o  33222  cycpmconjv  33402  cyc3evpm  33410  lindflbs  33635  matunitlindflem2  38155  eldioph2lem2  43383  f1cof1b  47702  fundcmpsurinj  48046  fundcmpsurbijinj  48047  fargshiftf1  48078  upgrimtrlslem2  48558  f102g  49514  f1mo  49515  aacllem  50474