Theorem f1eq1 6766

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 6680	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5853	. . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺)
3	2	funeqd 6555	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)))
5		df-f1 6538	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
6		df-f1 6538	. 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 5654  Fun wfun 6527  ⟶wf 6529  –1-1→wf1 6530

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538

This theorem is used by:  f1oeq1  6805  f1eq123d  6809  fo00  6854  f1prex  7285  f1iun  7941  tposf12  8249  oacomf1olem  8551  f1dom4g  8971  f1dom3g  8973  f1domg  8977  dom3d  9000  domtr  9013  0domg  9102  domssex2  9135  marypha1lem  9403  fseqenlem1  10027  dfac12lem2  10147  dfac12lem3  10148  ackbij2  10244  fin23lem28  10342  fin23lem32  10346  fin23lem34  10348  fin23lem35  10349  fin23lem41  10354  iundom2g  10548  pwfseqlem5  10672  hashf1lem1  14520  hashf1lem2  14521  hashf1  14522  4sqlem11  17047  injsubmefmnd  19006  conjsubgen  19378  sylow1lem2  19726  sylow2blem1  19747  hauspwpwf1  24213  oldfib  28642  istrkg2ld  28801  axlowdim  29418  sizusglecusg  29923  specval  32379  aciunf1lem  33135  zrhchr  34484  qqhre  34530  vonf1oonf1  35711  hashnexinj  42994  eldioph2lem2  43606  meadjiunlem  47293  fcoresf1b  47958  fundcmpsurbijinjpreimafv  48307  fundcmpsurinjpreimafv  48308  fundcmpsurinjimaid  48311  f1sn2g  49779  f102g  49780