Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-bdcel Unicode version

Theorem bj-bdcel 11071
 Description: Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
Hypothesis
Ref Expression
bj-bdcel.bd BOUNDED
Assertion
Ref Expression
bj-bdcel BOUNDED
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem bj-bdcel
StepHypRef Expression
1 bj-bdcel.bd . . 3 BOUNDED
21ax-bdex 11053 . 2 BOUNDED
3 risset 2400 . 2
42, 3bd0r 11059 1 BOUNDED
 Colors of variables: wff set class Syntax hints:   wceq 1285   wcel 1434  wrex 2354  BOUNDED wbd 11046 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468  ax-bd0 11047  ax-bdex 11053 This theorem depends on definitions:  df-bi 115  df-clel 2079  df-rex 2359 This theorem is referenced by:  bj-bd0el  11102  bj-bdsucel  11116
 Copyright terms: Public domain W3C validator