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

Theorem bdel 14219
Description: The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
Assertion
Ref Expression
bdel (BOUNDED 𝐴BOUNDED 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem bdel
StepHypRef Expression
1 df-bdc 14215 . 2 (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥𝐴)
2 sp 1511 . 2 (∀𝑥BOUNDED 𝑥𝐴BOUNDED 𝑥𝐴)
31, 2sylbi 121 1 (BOUNDED 𝐴BOUNDED 𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351  wcel 2148  BOUNDED wbd 14186  BOUNDED wbdc 14214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-bdc 14215
This theorem is referenced by:  bdeli  14220
  Copyright terms: Public domain W3C validator