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

Theorem f1oeq2 6838
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 6801 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6818 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 6570 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 6570 . 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 1537  1-1wf1 6560  ontowfo 6561  1-1-ontowf1o 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570
This theorem is referenced by:  f1oeq23  6840  f1oeq123d  6843  f1oeq2d  6845  resin  6871  isoeq4  7340  breng  8993  f1dmvrnfibi  9379  cnfcom  9738  infxpenc2  10060  fsumf1o  15756  sumsnf  15776  fprodf1o  15979  prodsn  15995  prodsnf  15997  znhash  21595  znunithash  21601  imasf1oxms  24518  wlksnwwlknvbij  29938  clwwlkvbij  30142  eupthp1  30245  derangval  35152  subfacp1lem2a  35165  subfacp1lem3  35167  subfacp1lem5  35169  sumsnd  44964  isuspgrim0lem  47809  isubgr3stgrlem1  47869  usgrexmpl1lem  47916  usgrexmpl2lem  47921  uspgrsprfo  47992
  Copyright terms: Public domain W3C validator