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 5850	. . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺)
3	2	funeqd 6561	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)))
5		df-f1 6543	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
6		df-f1 6543	. 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 5649  Fun wfun 6532  ⟶wf 6534  –1-1→wf1 6535

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 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543

This theorem is used by:  f1oeq1  6812  f1eq123d  6816  fo00  6861  f1prex  7292  f1iun  7956  tposf12  8268  oacomf1olem  8572  f1dom4g  8992  f1dom3g  8994  f1domg  8998  dom3d  9021  domtr  9034  0domg  9123  domssex2  9156  marypha1lem  9425  fseqenlem1  10103  dfac12lem2  10223  dfac12lem3  10224  ackbij2  10320  fin23lem28  10418  fin23lem32  10422  fin23lem34  10424  fin23lem35  10425  fin23lem41  10430  iundom2g  10624  pwfseqlem5  10748  hashf1lem1  14600  hashf1lem2  14601  hashf1  14602  4sqlem11  17133  injsubmefmnd  19093  conjsubgen  19465  sylow1lem2  19813  sylow2blem1  19834  hauspwpwf1  24306  oldfib  28763  istrkg2ld  28922  axlowdim  29539  sizusglecusg  30044  specval  32500  aciunf1lem  33256  zrhchr  34606  qqhre  34652  vonf1oonf1  35893  hashnexinj  43179  eldioph2lem2  43772  meadjiunlem  47475  fcoresf1b  48140  fundcmpsurbijinjpreimafv  48489  fundcmpsurinjpreimafv  48490  fundcmpsurinjimaid  48493  f1sn2g  49961  f102g  49962