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	$$⊢\left(\iota x\in A|\phi \right)=if\left(\exists !x\in A\phi ,\left(\iota x|\left(x\in A\wedge \phi \right)\right),\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	crio	$$class\left(\iota x\in A|\phi \right)$$
4	2 0 1	wreu	$$wff\exists !x\in A\phi$$
5	0	cv	$$setvarx$$
6	5 1	wcel	$$wffx\in A$$
7	6 2	wa	$$wff\left(x\in A\wedge \phi \right)$$
8	7 0	cio	$$class\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
9		cund	$$class\mathrm{Undef}$$
10	6 0	cab	$$class\left\{x|x\in A\right\}$$
11	10 9	cfv	$$class\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)$$
12	4 8 11	cif	$$classif\left(\exists !x\in A\phi ,\left(\iota x|\left(x\in A\wedge \phi \right)\right),\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)\right)$$
13	3 12	wceq	$$wff\left(\iota x\in A|\phi \right)=if\left(\exists !x\in A\phi ,\left(\iota x|\left(x\in A\wedge \phi \right)\right),\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)\right)$$