Axiom ax-riotaBAD 33257

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 5768. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6511, CONFLICTS WITH (THE NEW) df-riota 6511 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 6510	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	1, 2, 3	wreu 2898	. . 3 wff ∃!𝑥 ∈ 𝐴 𝜑
6	2	cv 1474	. . . . . 6 class 𝑥
7	6, 3	wcel 1977	. . . . 5 wff 𝑥 ∈ 𝐴
8	7, 1	wa 383	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
9	8, 2	cio 5766	. . 3 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
10	7, 2	cab 2596	. . . 4 class {𝑥 ∣ 𝑥 ∈ 𝐴}
11		cund 7285	. . . 4 class Undef
12	10, 11	cfv 5804	. . 3 class (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴})
13	5, 9, 12	cif 4036	. 2 class if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))
14	4, 13	wceq 1475	1 wff (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴}))

This axiom is referenced by:  riotaclbgBAD  33258