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

Theorem f1eq1 5989
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 5920 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
2 cnveq 5201 . . . 4 (𝐹 = 𝐺𝐹 = 𝐺)
32funeqd 5806 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
41, 3anbi12d 742 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴𝐵 ∧ Fun 𝐹) ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺)))
5 df-f1 5790 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
6 df-f1 5790 . 2 (𝐺:𝐴1-1𝐵 ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺))
74, 5, 63bitr4g 301 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  ccnv 5022  Fun wfun 5779  wf 5781  1-1wf1 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-rab 2899  df-v 3169  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-br 4573  df-opab 4633  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790
This theorem is referenced by:  f1oeq1  6020  f1eq123d  6024  fo00  6064  f1prex  6412  fun11iun  6991  tposf12  7236  oacomf1olem  7503  f1dom2g  7831  f1domg  7833  dom3d  7855  domtr  7867  domssex2  7977  1sdom  8020  marypha1lem  8194  fseqenlem1  8702  dfac12lem2  8821  dfac12lem3  8822  ackbij2  8920  fin23lem28  9017  fin23lem32  9021  fin23lem34  9023  fin23lem35  9024  fin23lem41  9029  iundom2g  9213  pwfseqlem5  9336  hashf1lem1  13043  hashf1lem2  13044  hashf1  13045  4sqlem11  15438  conjsubgen  17457  sylow1lem2  17778  sylow2blem1  17799  hauspwpwf1  21538  istrkg2ld  25071  axlowdim  25554  isuslgra  25633  isusgra  25634  usgrares  25659  sizeusglecusg  25775  2trllemE  25844  constr1trl  25879  specval  27942  aciunf1lem  28645  zrhchr  29149  qqhre  29193  eldioph2lem2  36140  meadjiunlem  39157  sizusglecusg  40676
  Copyright terms: Public domain W3C validator