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

Theorem f1oeq23 6839
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 6837 . 2 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
2 f1oeq3 6838 . 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 1540  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-ss 3968  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568
This theorem is referenced by:  f1ofvswap  7326  enfixsn  9121  ackbij2lem2  10279  seqf1o  14084  eulerthlem2  16819  isgim  19280  islmim  21061  fpwrelmapffs  32745  wrdpmcl  32922  1arithidomlem2  33564  1arithidom  33565  hgt750lemg  34669  poimirlem3  37630  poimirlem15  37642  eldioph2lem1  42771  fundcmpsurbijinj  47397  gricushgr  47886  isgrlim  47949
  Copyright terms: Public domain W3C validator