Metamath Proof Explorer


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 ( 𝑥𝐴 𝜑 ) = if ( ∃! 𝑥𝐴 𝜑 , ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) ) , ( Undef ‘ { 𝑥𝑥𝐴 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 𝑥
1 cA 𝐴
2 wph 𝜑
3 2 0 1 crio ( 𝑥𝐴 𝜑 )
4 2 0 1 wreu ∃! 𝑥𝐴 𝜑
5 0 cv 𝑥
6 5 1 wcel 𝑥𝐴
7 6 2 wa ( 𝑥𝐴𝜑 )
8 7 0 cio ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) )
9 cund Undef
10 6 0 cab { 𝑥𝑥𝐴 }
11 10 9 cfv ( Undef ‘ { 𝑥𝑥𝐴 } )
12 4 8 11 cif if ( ∃! 𝑥𝐴 𝜑 , ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) ) , ( Undef ‘ { 𝑥𝑥𝐴 } ) )
13 3 12 wceq ( 𝑥𝐴 𝜑 ) = if ( ∃! 𝑥𝐴 𝜑 , ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) ) , ( Undef ‘ { 𝑥𝑥𝐴 } ) )