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

Theorem f1oeq2 6837
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 6800 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6817 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 6568 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 6568 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  1-1wf1 6558  ontowfo 6559  1-1-ontowf1o 6560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568
This theorem is referenced by:  f1oeq23  6839  f1oeq123d  6842  f1oeq2d  6844  resin  6870  isoeq4  7340  breng  8994  f1dmvrnfibi  9381  cnfcom  9740  infxpenc2  10062  fsumf1o  15759  sumsnf  15779  fprodf1o  15982  prodsn  15998  prodsnf  16000  znhash  21577  znunithash  21583  imasf1oxms  24502  wlksnwwlknvbij  29928  clwwlkvbij  30132  eupthp1  30235  derangval  35172  subfacp1lem2a  35185  subfacp1lem3  35187  subfacp1lem5  35189  sumsnd  45031  isuspgrim0lem  47871  isubgr3stgrlem1  47933  usgrexmpl1lem  47980  usgrexmpl2lem  47985  uspgrsprfo  48064  tposf1o  48784
  Copyright terms: Public domain W3C validator