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

Theorem f1oeq3 6167
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq3 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))

Proof of Theorem f1oeq3
StepHypRef Expression
1 f1eq3 6136 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶1-1𝐴𝐹:𝐶1-1𝐵))
2 foeq3 6151 . . 3 (𝐴 = 𝐵 → (𝐹:𝐶onto𝐴𝐹:𝐶onto𝐵))
31, 2anbi12d 747 . 2 (𝐴 = 𝐵 → ((𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴) ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵)))
4 df-f1o 5933 . 2 (𝐹:𝐶1-1-onto𝐴 ↔ (𝐹:𝐶1-1𝐴𝐹:𝐶onto𝐴))
5 df-f1o 5933 . 2 (𝐹:𝐶1-1-onto𝐵 ↔ (𝐹:𝐶1-1𝐵𝐹:𝐶onto𝐵))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933
This theorem is referenced by:  f1oeq23  6168  f1oeq123d  6171  f1oeq3d  6172  f1ores  6189  resin  6196  f1osng  6215  f1oresrab  6435  fveqf1o  6597  isoeq5  6611  isoini2  6629  ncanth  6649  oacomf1o  7690  mapsnf1o  7991  bren  8006  xpcomf1o  8090  domss2  8160  isinf  8214  wemapwe  8632  oef1o  8633  cnfcomlem  8634  cnfcom2  8637  cnfcom3  8639  cnfcom3clem  8640  infxpenc  8879  infxpenc2lem1  8880  infxpenc2  8883  fin1a2lem6  9265  hsmexlem1  9286  pwfseqlem5  9523  pwfseq  9524  hashgf1o  12810  axdc4uzlem  12822  sumeq1  14463  fsumss  14500  fsumcnv  14548  prodeq1f  14682  fprodss  14722  fprodcnv  14757  unbenlem  15659  4sqlem11  15706  pwssnf1o  16205  catcisolem  16803  yoniso  16972  gsumvalx  17317  gsumpropd  17319  gsumpropd2lem  17320  xpsmnd  17377  xpsgrp  17581  cayley  17880  cayleyth  17881  gsumval3lem1  18352  gsumval3lem2  18353  gsumcom2  18420  scmatrngiso  20390  m2cpmrngiso  20611  cncfcnvcn  22771  ovolicc2lem4  23334  logf1o2  24441  uspgrf1oedg  26113  wlkiswwlks2lem4  26826  clwwlkvbijOLD  27089  adjbd1o  29072  rinvf1o  29560  eulerpartgbij  30562  eulerpartlemgh  30568  derangval  31275  subfacp1lem2a  31288  subfacp1lem3  31290  subfacp1lem5  31292  mrsubff1o  31538  msubff1o  31580  bj-finsumval0  33277  f1omptsnlem  33313  f1omptsn  33314  poimirlem4  33543  poimirlem9  33548  poimirlem15  33554  ismtyval  33729  ismrer1  33767  rngoisoval  33906  lautset  35686  pautsetN  35702  hvmap1o2  37371  pwfi2f1o  37983  imasgim  37987  uspgrsprfo  42081
  Copyright terms: Public domain W3C validator