Theorem f1eq2 6724

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 6639	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6495	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6495	. 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 5621  Fun wfun 6484  ⟶wf 6486  –1-1→wf1 6487

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6493  df-f 6494  df-f1 6495

This theorem is referenced by:  f1co  6739  f1oeq2  6761  f1eq123d  6764  f10d  6806  brdom2g  8895  marypha1lem  9337  fseqenlem1  9935  dfac12lem2  10056  dfac12lem3  10057  ackbij2  10153  iundom2g  10451  hashf1  14381  istrkg3ld  28517  ausgrusgrb  29222  usgr0  29300  uspgr1e  29301  usgrres  29365  usgrexilem  29497  usgr2pthlem  29820  usgr2pth  29821  s2f1  33010  ccatf1  33014  cshf1o  33027  cycpmconjv  33208  cyc3evpm  33216  lindflbs  33444  matunitlindflem2  37929  eldioph2lem2  43192  f1cof1b  47511  fundcmpsurinj  47843  fundcmpsurbijinj  47844  fargshiftf1  47875  upgrimtrlslem2  48339  f102g  49285  f1mo  49286  aacllem  50234