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

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

Proof of Theorem f1oeq2
StepHypRef Expression
1 f1eq2 6783 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6802 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 631 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 6550 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 6550 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 313 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  1-1wf1 6540  ontowfo 6541  1-1-ontowf1o 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550
This theorem is referenced by:  f1oeq23  6824  f1oeq123d  6827  f1oeq2d  6829  resin  6855  isoeq4  7319  breng  8950  brenOLD  8952  f1dmvrnfibi  9338  cnfcom  9697  infxpenc2  10019  fsumf1o  15673  sumsnf  15693  fprodf1o  15894  prodsn  15910  prodsnf  15912  znhash  21333  znunithash  21339  imasf1oxms  24218  wlksnwwlknvbij  29417  clwwlkvbij  29621  eupthp1  29724  derangval  34444  subfacp1lem2a  34457  subfacp1lem3  34459  subfacp1lem5  34461  sumsnd  44012  uspgrsprfo  46825
  Copyright terms: Public domain W3C validator