Definition df-riota 5560

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.

Assertion

Ref	Expression
df-riota	|- (iota_x e. Aph) = if(E!x e. A ph, (iotax(x e. A /\ ph)), (Undef` A))

Detailed syntax breakdown of Definition df-riota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	crio 5555	. 2 class (iota_x e. Aph)
5	1, 2, 3	wreu 2107	. . 3 wff E!x e. A ph
6	2	cv 1297	. . . . . 6 class x
7	6, 3	wcel 1300	. . . . 5 wff x e. A
8	7, 1	wa 240	. . . 4 wff (x e. A /\ ph)
9	8, 2	cio 5087	. . 3 class (iotax(x e. A /\ ph))
10		cund 5554	. . . 4 class Undef
11	3, 10	cfv 3998	. . 3 class (Undef` A)
12	5, 9, 11	cif 2982	. 2 class if(E!x e. A ph, (iotax(x e. A /\ ph)), (Undef` A))
13	4, 12	wceq 1298	1 wff (iota_x e. Aph) = if(E!x e. A ph, (iotax(x e. A /\ ph)), (Undef` A))

This definition is referenced by:  riotaeqdv 5561  riotabidv 5562  riotaex 5564  riotav 5565  riotaiota 5566  riotaprc 5567  hbriota1 5569  hbriota 5570  riotaund 5572  riotaclb 5573

Copyright terms: Public domain