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

Theorem bdinex1 7122
 Description: Bounded version of inex1 3865. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
bdinex1.bd BOUNDED
bdinex1.1
Assertion
Ref Expression
bdinex1

Proof of Theorem bdinex1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdinex1.1 . . . 4
2 bdinex1.bd . . . . . 6 BOUNDED
32bdeli 7073 . . . . 5 BOUNDED
43bdzfauscl 7116 . . . 4
51, 4ax-mp 7 . . 3
6 dfcleq 2016 . . . . 5
7 elin 3103 . . . . . . 7
87bibi2i 216 . . . . . 6
98albii 1339 . . . . 5
106, 9bitri 173 . . . 4
1110exbii 1478 . . 3
125, 11mpbir 134 . 2
1312issetri 2542 1
 Colors of variables: wff set class Syntax hints:   wa 97   wb 98  wal 1226   wceq 1228  wex 1362   wcel 1374  cvv 2535   cin 2893  BOUNDED wbdc 7067 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-bdsep 7111 This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2537  df-in 2901  df-bdc 7068 This theorem is referenced by:  bdinex2  7123  bdinex1g  7124  bdpeano5  7165
 Copyright terms: Public domain W3C validator