Theorem f1eq2 6719

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ^◡ccnv 5617  Fun wfun 6479  ⟶wf 6481  –1-1→wf1 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-fn 6488  df-f 6489  df-f1 6490

This theorem is referenced by:  f1co  6734  f1oeq2  6756  f1eq123d  6759  f10d  6801  brdom2g  8894  marypha1lem  9336  fseqenlem1  9937  dfac12lem2  10058  dfac12lem3  10059  ackbij2  10155  iundom2g  10453  hashf1  14410  istrkg3ld  28547  ausgrusgrb  29252  usgr0  29330  uspgr1e  29331  usgrres  29395  usgrexilem  29527  usgr2pthlem  29849  usgr2pth  29850  s2f1  33024  ccatf1  33028  cshf1o  33041  cycpmconjv  33223  cyc3evpm  33231  lindflbs  33462  matunitlindflem2  37984  eldioph2lem2  43210  f1cof1b  47540  fundcmpsurinj  47884  fundcmpsurbijinj  47885  fargshiftf1  47916  upgrimtrlslem2  48396  f102g  49342  f1mo  49343  aacllem  50291