Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdctp GIF version

Theorem bdctp 13285
 Description: The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
Assertion
Ref Expression
bdctp BOUNDED {𝑥, 𝑦, 𝑧}

Proof of Theorem bdctp
StepHypRef Expression
1 bdcpr 13284 . . 3 BOUNDED {𝑥, 𝑦}
2 bdcsn 13283 . . 3 BOUNDED {𝑧}
31, 2bdcun 13275 . 2 BOUNDED ({𝑥, 𝑦} ∪ {𝑧})
4 df-tp 3541 . 2 {𝑥, 𝑦, 𝑧} = ({𝑥, 𝑦} ∪ {𝑧})
53, 4bdceqir 13257 1 BOUNDED {𝑥, 𝑦, 𝑧}
 Colors of variables: wff set class Syntax hints:   ∪ cun 3075  {csn 3533  {cpr 3534  {ctp 3535  BOUNDED wbdc 13253 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-bd0 13226  ax-bdor 13229  ax-bdeq 13233  ax-bdsb 13235 This theorem depends on definitions:  df-bi 116  df-clab 2127  df-cleq 2133  df-clel 2136  df-un 3081  df-sn 3539  df-pr 3540  df-tp 3541  df-bdc 13254 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator