Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bd0r Unicode version

Theorem bd0r 13023
Description: A formula equivalent to a bounded one is bounded. Stated with a commuted (compared with bd0 13022) biconditional in the hypothesis, to work better with definitions (
ps is the definiendum that one wants to prove bounded). (Contributed by BJ, 3-Oct-2019.)
Hypotheses
Ref Expression
bd0r.min  |- BOUNDED  ph
bd0r.maj  |-  ( ps  <->  ph )
Assertion
Ref Expression
bd0r  |- BOUNDED  ps

Proof of Theorem bd0r
StepHypRef Expression
1 bd0r.min . 2  |- BOUNDED  ph
2 bd0r.maj . . 3  |-  ( ps  <->  ph )
32bicomi 131 . 2  |-  ( ph  <->  ps )
41, 3bd0 13022 1  |- BOUNDED  ps
Colors of variables: wff set class
Syntax hints:    <-> wb 104  BOUNDED wbd 13010
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-bd0 13011
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bdbi  13024  bdstab  13025  bddc  13026  bd3or  13027  bd3an  13028  bdfal  13031  bdxor  13034  bj-bdcel  13035  bdab  13036  bdcdeq  13037  bdne  13051  bdnel  13052  bdreu  13053  bdrmo  13054  bdsbcALT  13057  bdss  13062  bdeq0  13065  bdvsn  13072  bdop  13073  bdeqsuc  13079  bj-bdind  13128
  Copyright terms: Public domain W3C validator