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