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 ‘ { 𝑥 ∣ 𝑥 ∈ 𝐴 } ) )

Metamath Proof Explorer

Axiom ax-riotaBAD

Detailed syntax breakdown