Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-riotaBAD Structured version   Visualization version   GIF version

Axiom ax-riotaBAD 35971
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 6308. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7103, CONFLICTS WITH (THE NEW) df-riota 7103 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
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3crio 7102 . 2 class (𝑥𝐴 𝜑)
51, 2, 3wreu 3140 . . 3 wff ∃!𝑥𝐴 𝜑
62cv 1527 . . . . . 6 class 𝑥
76, 3wcel 2105 . . . . 5 wff 𝑥𝐴
87, 1wa 396 . . . 4 wff (𝑥𝐴𝜑)
98, 2cio 6306 . . 3 class (℩𝑥(𝑥𝐴𝜑))
107, 2cab 2799 . . . 4 class {𝑥𝑥𝐴}
11 cund 7929 . . . 4 class Undef
1210, 11cfv 6349 . . 3 class (Undef‘{𝑥𝑥𝐴})
135, 9, 12cif 4465 . 2 class if(∃!𝑥𝐴 𝜑, (℩𝑥(𝑥𝐴𝜑)), (Undef‘{𝑥𝑥𝐴}))
144, 13wceq 1528 1 wff (𝑥𝐴 𝜑) = if(∃!𝑥𝐴 𝜑, (℩𝑥(𝑥𝐴𝜑)), (Undef‘{𝑥𝑥𝐴}))
Colors of variables: wff setvar class
This axiom is referenced by:  riotaclbgBAD  35972
  Copyright terms: Public domain W3C validator