Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-xdiv Structured version   Unicode version

Definition df-xdiv 27766
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
StepHypRef Expression
1 cxdiv 27765 . 2  class /𝑒
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9644 . . 3  class  RR*
5 cr 9508 . . . 4  class  RR
6 cc0 9509 . . . . 5  class  0
76csn 4032 . . . 4  class  { 0 }
85, 7cdif 3468 . . 3  class  ( RR 
\  { 0 } )
93cv 1394 . . . . . 6  class  y
10 vz . . . . . . 7  setvar  z
1110cv 1394 . . . . . 6  class  z
12 cxmu 11342 . . . . . 6  class  xe
139, 11, 12co 6296 . . . . 5  class  ( y xe z )
142cv 1394 . . . . 5  class  x
1513, 14wceq 1395 . . . 4  wff  ( y xe z )  =  x
1615, 10, 4crio 6257 . . 3  class  ( iota_ z  e.  RR*  ( y xe z )  =  x )
172, 3, 4, 8, 16cmpt2 6298 . 2  class  ( x  e.  RR* ,  y  e.  ( RR  \  {
0 } )  |->  (
iota_ z  e.  RR*  (
y xe z )  =  x ) )
181, 17wceq 1395 1  wff /𝑒  =  ( x  e.  RR* ,  y  e.  ( RR  \  {
0 } )  |->  (
iota_ z  e.  RR*  (
y xe z )  =  x ) )
Colors of variables: wff setvar class
This definition is referenced by:  xdivval  27767
  Copyright terms: Public domain W3C validator