Metamath Proof Explorer


Axiom ax-riotaBAD

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 . (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 15-Oct-2016) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota , CONFLICTS WITH (THE NEW) df-riota AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.

Ref Expression
Assertion 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

Step Hyp Ref Expression
0 vx
 |-  x
1 cA
 |-  A
2 wph
 |-  ph
3 2 0 1 crio
 |-  ( iota_ x e. A ph )
4 2 0 1 wreu
 |-  E! x e. A ph
5 0 cv
 |-  x
6 5 1 wcel
 |-  x e. A
7 6 2 wa
 |-  ( x e. A /\ ph )
8 7 0 cio
 |-  ( iota x ( x e. A /\ ph ) )
9 cund
 |-  Undef
10 6 0 cab
 |-  { x | x e. A }
11 10 9 cfv
 |-  ( Undef ` { x | x e. A } )
12 4 8 11 cif
 |-  if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )
13 3 12 wceq
 |-  ( iota_ x e. A ph ) = if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )