Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdeli Structured version   GIF version

Theorem bdeli 9281
Description: Inference associated with bdel 9280. Its converse is bdelir 9282. (Contributed by BJ, 3-Oct-2019.)
Hypothesis
Ref Expression
bdeli.1 BOUNDED A
Assertion
Ref Expression
bdeli BOUNDED x A
Distinct variable group:   x,A

Proof of Theorem bdeli
StepHypRef Expression
1 bdeli.1 . 2 BOUNDED A
2 bdel 9280 . 2 (BOUNDED ABOUNDED x A)
31, 2ax-mp 7 1 BOUNDED x A
Colors of variables: wff set class
Syntax hints:   wcel 1390  BOUNDED wbd 9247  BOUNDED wbdc 9275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1397
This theorem depends on definitions:  df-bi 110  df-bdc 9276
This theorem is referenced by:  bdph  9285  bdcrab  9287  bdnel  9289  bdccsb  9295  bdcdif  9296  bdcun  9297  bdcin  9298  bdss  9299  bdsnss  9308  bdciun  9313  bdciin  9314  bdinex1  9330  bj-uniex2  9347  bj-inf2vnlem3  9402
  Copyright terms: Public domain W3C validator