Theorem f1eq2 6732

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ^◡ccnv 5630  Fun wfun 6492  ⟶wf 6494  –1-1→wf1 6495

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501  df-f 6502  df-f1 6503

This theorem is referenced by:  f1co  6747  f1oeq2  6769  f1eq123d  6772  f10d  6814  brdom2g  8904  marypha1lem  9346  fseqenlem1  9946  dfac12lem2  10067  dfac12lem3  10068  ackbij2  10164  iundom2g  10462  hashf1  14419  istrkg3ld  28529  ausgrusgrb  29234  usgr0  29312  uspgr1e  29313  usgrres  29377  usgrexilem  29509  usgr2pthlem  29831  usgr2pth  29832  s2f1  33005  ccatf1  33009  cshf1o  33022  cycpmconjv  33203  cyc3evpm  33211  lindflbs  33439  matunitlindflem2  37938  eldioph2lem2  43193  f1cof1b  47525  fundcmpsurinj  47869  fundcmpsurbijinj  47870  fargshiftf1  47901  upgrimtrlslem2  48381  f102g  49327  f1mo  49328  aacllem  50276