Theorem f1eq1 6773

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 6687	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5861	. . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺)
3	2	funeqd 6562	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)))
5		df-f1 6545	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
6		df-f1 6545	. 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 1570  ^◡ccnv 5662  Fun wfun 6534  ⟶wf 6536  –1-1→wf1 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545

This theorem is used by:  f1oeq1  6812  f1eq123d  6816  fo00  6861  f1prex  7291  f1iun  7947  tposf12  8253  oacomf1olem  8555  f1dom4g  8968  f1dom3g  8970  f1domg  8974  dom3d  8997  domtr  9010  0domg  9099  domssex2  9132  marypha1lem  9400  fseqenlem1  10024  dfac12lem2  10144  dfac12lem3  10145  ackbij2  10241  fin23lem28  10339  fin23lem32  10343  fin23lem34  10345  fin23lem35  10346  fin23lem41  10351  iundom2g  10539  pwfseqlem5  10663  hashf1lem1  14510  hashf1lem2  14511  hashf1  14512  4sqlem11  17037  injsubmefmnd  18993  conjsubgen  19365  sylow1lem2  19713  sylow2blem1  19734  hauspwpwf1  24195  oldfib  28621  istrkg2ld  28780  axlowdim  29366  sizusglecusg  29871  specval  32321  aciunf1lem  33078  zrhchr  34428  qqhre  34474  vonf1oonf1  35655  hashnexinj  42953  eldioph2lem2  43550  meadjiunlem  47237  fcoresf1b  47865  fundcmpsurbijinjpreimafv  48214  fundcmpsurinjpreimafv  48215  fundcmpsurinjimaid  48218  f1sn2g  49686  f102g  49687