Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-riotaBAD Structured version   Unicode version

Axiom ax-riotaBAD 33774
Description: Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse  A. See also comments for df-iota 5551. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6245, CONFLICTS WITH (THE NEW) df-riota 6245 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.
Assertion
Ref Expression
ax-riotaBAD  |-  ( iota_ x  e.  A  ph )  =  if ( E! x  e.  A  ph ,  ( iota x ( x  e.  A  /\  ph ) ) ,  (
Undef `  { x  |  x  e.  A }
) )

Detailed syntax breakdown of Axiom ax-riotaBAD
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3crio 6244 . 2  class  ( iota_ x  e.  A  ph )
51, 2, 3wreu 2816 . . 3  wff  E! x  e.  A  ph
62cv 1378 . . . . . 6  class  x
76, 3wcel 1767 . . . . 5  wff  x  e.  A
87, 1wa 369 . . . 4  wff  ( x  e.  A  /\  ph )
98, 2cio 5549 . . 3  class  ( iota
x ( x  e.  A  /\  ph )
)
107, 2cab 2452 . . . 4  class  { x  |  x  e.  A }
11 cund 7001 . . . 4  class  Undef
1210, 11cfv 5588 . . 3  class  ( Undef `  { x  |  x  e.  A } )
135, 9, 12cif 3939 . 2  class  if ( E! x  e.  A  ph ,  ( iota x
( x  e.  A  /\  ph ) ) ,  ( Undef `  { x  |  x  e.  A } ) )
144, 13wceq 1379 1  wff  ( iota_ x  e.  A  ph )  =  if ( E! x  e.  A  ph ,  ( iota x ( x  e.  A  /\  ph ) ) ,  (
Undef `  { x  |  x  e.  A }
) )
Colors of variables: wff setvar class
This axiom is referenced by:  riotaclbgBAD  33775  riotaclbBAD  33776
  Copyright terms: Public domain W3C validator