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

Theorem bdcriota 13272
 Description: A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
Hypotheses
Ref Expression
bdcriota.bd BOUNDED
bdcriota.ex
Assertion
Ref Expression
bdcriota BOUNDED
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem bdcriota
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdcriota.bd . . . . . . . . 9 BOUNDED
21ax-bdsb 13211 . . . . . . . 8 BOUNDED
3 ax-bdel 13210 . . . . . . . 8 BOUNDED
42, 3ax-bdim 13203 . . . . . . 7 BOUNDED
54ax-bdal 13207 . . . . . 6 BOUNDED
6 df-ral 2422 . . . . . . . . 9
7 impexp 261 . . . . . . . . . . 11
87bicomi 131 . . . . . . . . . 10
98albii 1447 . . . . . . . . 9
106, 9bitri 183 . . . . . . . 8
11 sban 1929 . . . . . . . . . . . 12
12 clelsb3 2245 . . . . . . . . . . . . 13
1312anbi1i 454 . . . . . . . . . . . 12
1411, 13bitri 183 . . . . . . . . . . 11
1514bicomi 131 . . . . . . . . . 10
1615imbi1i 237 . . . . . . . . 9
1716albii 1447 . . . . . . . 8
1810, 17bitri 183 . . . . . . 7
19 df-clab 2127 . . . . . . . . . 10
2019bicomi 131 . . . . . . . . 9
2120imbi1i 237 . . . . . . . 8
2221albii 1447 . . . . . . 7
2318, 22bitri 183 . . . . . 6
245, 23bd0 13213 . . . . 5 BOUNDED
2524bdcab 13238 . . . 4 BOUNDED
26 df-int 3781 . . . 4
2725, 26bdceqir 13233 . . 3 BOUNDED
28 bdcriota.ex . . . . 5
29 df-reu 2424 . . . . 5
3028, 29mpbi 144 . . . 4
31 iotaint 5110 . . . 4
3230, 31ax-mp 5 . . 3
3327, 32bdceqir 13233 . 2 BOUNDED
34 df-riota 5739 . 2
3533, 34bdceqir 13233 1 BOUNDED
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103  wal 1330   wceq 1332   wcel 1481  wsb 1736  weu 2000  cab 2126  wral 2417  wreu 2419  cint 3780  cio 5095  crio 5738  BOUNDED wbd 13201  BOUNDED wbdc 13229 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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-bd0 13202  ax-bdim 13203  ax-bdal 13207  ax-bdel 13210  ax-bdsb 13211 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-reu 2424  df-v 2692  df-sbc 2915  df-un 3081  df-in 3083  df-sn 3539  df-pr 3540  df-uni 3746  df-int 3781  df-iota 5097  df-riota 5739  df-bdc 13230 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator