Theorem f1eq2 6727

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 6642	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6498	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6498	. 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 5624  Fun wfun 6487  ⟶wf 6489  –1-1→wf1 6490

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 6496  df-f 6497  df-f1 6498

This theorem is referenced by:  f1co  6742  f1oeq2  6764  f1eq123d  6767  f10d  6809  brdom2g  8898  marypha1lem  9340  fseqenlem1  9940  dfac12lem2  10061  dfac12lem3  10062  ackbij2  10158  iundom2g  10456  hashf1  14413  istrkg3ld  28546  ausgrusgrb  29251  usgr0  29329  uspgr1e  29330  usgrres  29394  usgrexilem  29526  usgr2pthlem  29849  usgr2pth  29850  s2f1  33023  ccatf1  33027  cshf1o  33040  cycpmconjv  33221  cyc3evpm  33229  lindflbs  33457  matunitlindflem2  37955  eldioph2lem2  43210  f1cof1b  47540  fundcmpsurinj  47884  fundcmpsurbijinj  47885  fargshiftf1  47916  upgrimtrlslem2  48396  f102g  49342  f1mo  49343  aacllem  50291