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

Theorem bdreu 13112
Description: Boundedness of existential uniqueness.

Remark regarding restricted quantifiers: the formula  A. x  e.  A ph need not be bounded even if 
A and  ph are. Indeed,  _V is bounded by bdcvv 13114, and  |-  ( A. x  e. 
_V ph  <->  A. x ph ) (in minimal propositional calculus), so by bd0 13081, if  A. x  e. 
_V ph were bounded when  ph is bounded, then  A. x ph would be bounded as well when  ph is bounded, which is not the case. The same remark holds with  E. ,  E! ,  E*. (Contributed by BJ, 16-Oct-2019.)

Hypothesis
Ref Expression
bdreu.1  |- BOUNDED  ph
Assertion
Ref Expression
bdreu  |- BOUNDED  E! x  e.  y 
ph
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem bdreu
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 bdreu.1 . . . 4  |- BOUNDED  ph
21ax-bdex 13076 . . 3  |- BOUNDED  E. x  e.  y 
ph
3 ax-bdeq 13077 . . . . . 6  |- BOUNDED  x  =  z
41, 3ax-bdim 13071 . . . . 5  |- BOUNDED  ( ph  ->  x  =  z )
54ax-bdal 13075 . . . 4  |- BOUNDED  A. x  e.  y  ( ph  ->  x  =  z )
65ax-bdex 13076 . . 3  |- BOUNDED  E. z  e.  y 
A. x  e.  y  ( ph  ->  x  =  z )
72, 6ax-bdan 13072 . 2  |- BOUNDED  ( E. x  e.  y  ph  /\  E. z  e.  y  A. x  e.  y  ( ph  ->  x  =  z ) )
8 reu3 2874 . 2  |-  ( E! x  e.  y  ph  <->  ( E. x  e.  y 
ph  /\  E. z  e.  y  A. x  e.  y  ( ph  ->  x  =  z ) ) )
97, 8bd0r 13082 1  |- BOUNDED  E! x  e.  y 
ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103   A.wral 2416   E.wrex 2417   E!wreu 2418  BOUNDED wbd 13069
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-bd0 13070  ax-bdim 13071  ax-bdan 13072  ax-bdal 13075  ax-bdex 13076  ax-bdeq 13077
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-cleq 2132  df-clel 2135  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424
This theorem is referenced by:  bdrmo  13113
  Copyright terms: Public domain W3C validator