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 } ) ) |
| 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 } ) ) |