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

Theorem f1eq1 6257
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 6187 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
2 cnveq 5451 . . . 4 (𝐹 = 𝐺𝐹 = 𝐺)
32funeqd 6071 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
41, 3anbi12d 749 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴𝐵 ∧ Fun 𝐹) ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺)))
5 df-f1 6054 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
6 df-f1 6054 . 2 (𝐺:𝐴1-1𝐵 ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺))
74, 5, 63bitr4g 303 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  ccnv 5265  Fun wfun 6043  wf 6045  1-1wf1 6046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054
This theorem is referenced by:  f1oeq1  6288  f1eq123d  6292  fo00  6333  f1prex  6702  fun11iun  7291  tposf12  7546  oacomf1olem  7813  f1dom2g  8139  f1domg  8141  dom3d  8163  domtr  8174  domssex2  8285  1sdom  8328  marypha1lem  8504  fseqenlem1  9037  dfac12lem2  9158  dfac12lem3  9159  ackbij2  9257  fin23lem28  9354  fin23lem32  9358  fin23lem34  9360  fin23lem35  9361  fin23lem41  9366  iundom2g  9554  pwfseqlem5  9677  hashf1lem1  13431  hashf1lem2  13432  hashf1  13433  4sqlem11  15861  conjsubgen  17894  sylow1lem2  18214  sylow2blem1  18235  hauspwpwf1  21992  istrkg2ld  25558  axlowdim  26040  sizusglecusg  26569  specval  29066  aciunf1lem  29771  zrhchr  30329  qqhre  30373  eldioph2lem2  37826  meadjiunlem  41185
  Copyright terms: Public domain W3C validator