Theorem f1eq1 6778

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 6692	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5852	. . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺)
3	2	funeqd 6566	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)))
5		df-f1 6548	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
6		df-f1 6548	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ^◡ccnv 5650  Fun wfun 6537  ⟶wf 6539  –1-1→wf1 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548

This theorem is used by:  f1oeq1  6817  f1eq123d  6821  fo00  6866  f1prex  7296  f1iun  7960  tposf12  8275  oacomf1olem  8579  f1dom4g  8999  f1dom3g  9001  f1domg  9005  dom3d  9028  domtr  9041  0domg  9130  domssex2  9163  marypha1lem  9432  fseqenlem1  10110  dfac12lem2  10230  dfac12lem3  10231  ackbij2  10327  fin23lem28  10425  fin23lem32  10429  fin23lem34  10431  fin23lem35  10432  fin23lem41  10437  iundom2g  10631  pwfseqlem5  10755  hashf1lem1  14607  hashf1lem2  14608  hashf1  14609  4sqlem11  17142  injsubmefmnd  19102  conjsubgen  19474  sylow1lem2  19822  sylow2blem1  19843  hauspwpwf1  24315  oldfib  28772  istrkg2ld  28931  axlowdim  29548  sizusglecusg  30053  specval  32509  aciunf1lem  33307  zrhchr  34656  qqhre  34702  vonf1oonf1  35966  onf1oracwevd  35975  onprcf1of1orad  35976  onprcf1of1orbd  35977  onprcf1of1ord  35978  hashnexinj  43287  eldioph2lem2  43881  meadjiunlem  47583  fcoresf1b  48248  fundcmpsurbijinjpreimafv  48597  fundcmpsurinjpreimafv  48598  fundcmpsurinjimaid  48601  f1sn2g  50070  f102g  50071