Axiom ax-riotaBAD 39990

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 𝐴. See also comments for df-iota 6493. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7375, CONFLICTS WITH (THE NEW) df-riota 7375 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	⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))

Detailed syntax breakdown of Axiom ax-riotaBAD

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	crio 7374	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	1, 2, 3	wreu 3364	. . 3 wff ∃!𝑥 ∈ 𝐴 𝜑
6	2	cv 1569	. . . . . 6 class 𝑥
7	6, 3	wcel 2145	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 401	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	8, 2	cio 6491	. . 3 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
10	7, 2	cab 2739	. . . 4 class {𝑥 ∣ 𝑥 ∈ 𝐴}
11		cund 8282	. . . 4 class Undef
12	10, 11	cfv 6537	. . 3 class (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴})
13	5, 9, 12	cif 4482	. 2 class if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))
14	4, 13	wceq 1570	1 wff (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))

This axiom is used by:  riotaclbgBAD  39991