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

Theorem f1oeq23 6840
Description: Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
Assertion
Ref Expression
f1oeq23 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐷))

Proof of Theorem f1oeq23
StepHypRef Expression
1 f1oeq2 6838 . 2 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
2 f1oeq3 6839 . 2 (𝐶 = 𝐷 → (𝐹:𝐵1-1-onto𝐶𝐹:𝐵1-1-onto𝐷))
31, 2sylan9bb 509 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  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-ss 3980  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570
This theorem is referenced by:  f1ofvswap  7326  enfixsn  9120  ackbij2lem2  10277  seqf1o  14081  eulerthlem2  16816  isgim  19293  islmim  21079  fpwrelmapffs  32752  wrdpmcl  32907  1arithidomlem2  33544  1arithidom  33545  hgt750lemg  34648  poimirlem3  37610  poimirlem15  37622  eldioph2lem1  42748  fundcmpsurbijinj  47335  gricushgr  47824  isgrlim  47885
  Copyright terms: Public domain W3C validator