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	$⊢ (ι x \in A \| φ) = if (\exists! x \in A φ, (ι x \| (x \in A \land φ)), Undef (\{x \| x \in A\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		cA	$class A$
2		wph	$wff φ$
3	2 0 1	crio	$class (ι x \in A \| φ)$
4	2 0 1	wreu	$wff \exists! x \in A φ$
5	0	cv	$setvar x$
6	5 1	wcel	$wff x \in A$
7	6 2	wa	$wff (x \in A \land φ)$
8	7 0	cio	$class (ι x \| (x \in A \land φ))$
9		cund	$class Undef$
10	6 0	cab	$class \{x \| x \in A\}$
11	10 9	cfv	$class Undef (\{x \| x \in A\})$
12	4 8 11	cif	$class if (\exists! x \in A φ, (ι x \| (x \in A \land φ)), Undef (\{x \| x \in A\}))$
13	3 12	wceq	$wff (ι x \in A \| φ) = if (\exists! x \in A φ, (ι x \| (x \in A \land φ)), Undef (\{x \| x \in A\}))$

Metamath Proof Explorer

Axiom ax-riotaBAD

Detailed syntax breakdown