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

Theorem f1eq1 6083
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 6013 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
2 cnveq 5285 . . . 4 (𝐹 = 𝐺𝐹 = 𝐺)
32funeqd 5898 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
41, 3anbi12d 746 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴𝐵 ∧ Fun 𝐹) ↔ (𝐺:𝐴𝐵 ∧ Fun 𝐺)))
5 df-f1 5881 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
6 df-f1 5881 . 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 384   = wceq 1481  ccnv 5103  Fun wfun 5870  wf 5872  1-1wf1 5873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881
This theorem is referenced by:  f1oeq1  6114  f1eq123d  6118  fo00  6159  f1prex  6524  fun11iun  7111  tposf12  7362  oacomf1olem  7629  f1dom2g  7958  f1domg  7960  dom3d  7982  domtr  7994  domssex2  8105  1sdom  8148  marypha1lem  8324  fseqenlem1  8832  dfac12lem2  8951  dfac12lem3  8952  ackbij2  9050  fin23lem28  9147  fin23lem32  9151  fin23lem34  9153  fin23lem35  9154  fin23lem41  9159  iundom2g  9347  pwfseqlem5  9470  hashf1lem1  13222  hashf1lem2  13223  hashf1  13224  4sqlem11  15640  conjsubgen  17674  sylow1lem2  17995  sylow2blem1  18016  hauspwpwf1  21772  istrkg2ld  25340  axlowdim  25822  sizusglecusg  26340  specval  28727  aciunf1lem  29435  zrhchr  29994  qqhre  30038  eldioph2lem2  37143  meadjiunlem  40445
  Copyright terms: Public domain W3C validator