Axiom ax-riotaBAD 32700

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 5402. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6073, CONFLICTS WITH (THE NEW) df-riota 6073 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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	crio 6072	. 2 class ( iota_ x e. A ph )
5	1, 2, 3	wreu 2738	. . 3 wff E! x e. A ph
6	2	cv 1368	. . . . . 6 class x
7	6, 3	wcel 1756	. . . . 5 wff x e. A
8	7, 1	wa 369	. . . 4 wff ( x e. A /\ ph )
9	8, 2	cio 5400	. . 3 class ( iota x ( x e. A /\ ph ) )
10	7, 2	cab 2429	. . . 4 class { x | x e. A }
11		cund 6812	. . . 4 class Undef
12	10, 11	cfv 5439	. . 3 class ( Undef ` { x | x e. A } )
13	5, 9, 12	cif 3812	. 2 class if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )
14	4, 13	wceq 1369	1 wff ( iota_ x e. A ph ) = if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )

This axiom is referenced by:  riotaclbgBAD  32701  riotaclbBAD  32702