Theorem f1eq1 6788

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)

Assertion

Ref	Expression
f1eq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Proof of Theorem f1eq1

Step	Hyp	Ref	Expression
1		feq1 6704	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5876	. . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺)
3	2	funeqd 6576	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)))
5		df-f1 6554	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
6		df-f1 6554	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺))
7	4, 5, 6	3bitr4g 313	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533  ^◡ccnv 5677  Fun wfun 6543  ⟶wf 6545  –1-1→wf1 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554

This theorem is referenced by:  f1oeq1  6826  f1eq123d  6830  fo00  6874  f1prex  7293  f1iun  7948  tposf12  8257  oacomf1olem  8585  f1dom4g  8986  f1dom3g  8988  f1dom2gOLD  8991  f1domg  8993  dom3d  9015  domtr  9028  0domg  9125  domssex2  9162  1sdomOLD  9274  marypha1lem  9458  fseqenlem1  10049  dfac12lem2  10169  dfac12lem3  10170  ackbij2  10268  fin23lem28  10365  fin23lem32  10369  fin23lem34  10371  fin23lem35  10372  fin23lem41  10377  iundom2g  10565  pwfseqlem5  10688  hashf1lem1  14451  hashf1lem1OLD  14452  hashf1lem2  14453  hashf1  14454  4sqlem11  16927  injsubmefmnd  18857  conjsubgen  19214  sylow1lem2  19566  sylow2blem1  19587  hauspwpwf1  23935  istrkg2ld  28336  axlowdim  28844  sizusglecusg  29349  specval  31780  aciunf1lem  32529  zrhchr  33708  qqhre  33752  hashnexinj  41731  eldioph2lem2  42323  meadjiunlem  45991  fcoresf1b  46590  fundcmpsurbijinjpreimafv  46884  fundcmpsurinjpreimafv  46885  fundcmpsurinjimaid  46888  f1sn2g  48089  f102g  48090