Theorem f1eq2 6734

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 6649	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
2	1	anbi1d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹) ↔ (𝐹:𝐵⟶𝐶 ∧ Fun ◡𝐹)))
3		df-f1 6505	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
4		df-f1 6505	. 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 5631  Fun wfun 6494  ⟶wf 6496  –1-1→wf1 6497

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 6503  df-f 6504  df-f1 6505

This theorem is referenced by:  f1co  6749  f1oeq2  6771  f1eq123d  6774  f10d  6816  brdom2g  8906  marypha1lem  9348  fseqenlem1  9946  dfac12lem2  10067  dfac12lem3  10068  ackbij2  10164  iundom2g  10462  hashf1  14392  istrkg3ld  28545  ausgrusgrb  29250  usgr0  29328  uspgr1e  29329  usgrres  29393  usgrexilem  29525  usgr2pthlem  29848  usgr2pth  29849  s2f1  33038  ccatf1  33042  cshf1o  33055  cycpmconjv  33236  cyc3evpm  33244  lindflbs  33472  matunitlindflem2  37868  eldioph2lem2  43118  f1cof1b  47437  fundcmpsurinj  47769  fundcmpsurbijinj  47770  fargshiftf1  47801  upgrimtrlslem2  48265  f102g  49211  f1mo  49212  aacllem  50160