MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1eq1 Structured version   Visualization version   GIF version

Theorem f1eq1 6430
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
StepHypRef Expression
1 feq1 6355 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
2 cnveq 5622 . . . 4 (𝐹 = 𝐺𝐹 = 𝐺)
32funeqd 6239 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
41, 3anbi12d 630 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴𝐵 ∧ Fun 𝐹) ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺)))
5 df-f1 6222 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
6 df-f1 6222 . 2 (𝐺:𝐴1-1𝐵 ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺))
74, 5, 63bitr4g 315 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1520  ccnv 5434  Fun wfun 6211  wf 6213  1-1wf1 6214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-br 4957  df-opab 5019  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222
This theorem is referenced by:  f1oeq1  6464  f1eq123d  6468  fo00  6510  f1prex  6896  fun11iun  7492  tposf12  7759  oacomf1olem  8031  f1dom2g  8365  f1domg  8367  dom3d  8389  domtr  8400  domssex2  8514  1sdom  8557  marypha1lem  8733  fseqenlem1  9285  dfac12lem2  9405  dfac12lem3  9406  ackbij2  9500  fin23lem28  9597  fin23lem32  9601  fin23lem34  9603  fin23lem35  9604  fin23lem41  9609  iundom2g  9797  pwfseqlem5  9920  hashf1lem1  13649  hashf1lem2  13650  hashf1  13651  4sqlem11  16108  conjsubgen  18120  sylow1lem2  18442  sylow2blem1  18463  hauspwpwf1  22267  istrkg2ld  25916  axlowdim  26418  sizusglecusg  26916  specval  29354  aciunf1lem  30070  zrhchr  30790  qqhre  30834  eldioph2lem2  38793  meadjiunlem  42243
  Copyright terms: Public domain W3C validator