Definition df-xdiv 29626

Description: Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.)

Assertion

Ref	Expression
df-xdiv	|- /𝑒 = ( x e. RR* , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR* ( y xe z ) = x ) )

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-xdiv

Step	Hyp	Ref	Expression
1		cxdiv 29625	. 2 class /𝑒
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 10073	. . 3 class RR*
5		cr 9935	. . . 4 class RR
6		cc0 9936	. . . . 5 class 0
7	6	csn 4177	. . . 4 class { 0 }
8	5, 7	cdif 3571	. . 3 class ( RR \ { 0 } )
9	3	cv 1482	. . . . . 6 class y
10		vz	. . . . . . 7 setvar z
11	10	cv 1482	. . . . . 6 class z
12		cxmu 11945	. . . . . 6 class xe
13	9, 11, 12	co 6650	. . . . 5 class ( y xe z )
14	2	cv 1482	. . . . 5 class x
15	13, 14	wceq 1483	. . . 4 wff ( y xe z ) = x
16	15, 10, 4	crio 6610	. . 3 class ( iota_ z e. RR* ( y xe z ) = x )
17	2, 3, 4, 8, 16	cmpt2 6652	. 2 class ( x e. RR* , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR* ( y xe z ) = x ) )
18	1, 17	wceq 1483	1 wff /𝑒 = ( x e. RR* , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR* ( y xe z ) = x ) )

This definition is referenced by:  xdivval  29627