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 26093
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 26092 . 2  class /𝑒
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 9417 . . 3  class  RR*
5 cr 9281 . . . 4  class  RR
6 cc0 9282 . . . . 5  class  0
76csn 3877 . . . 4  class  { 0 }
85, 7cdif 3325 . . 3  class  ( RR 
\  { 0 } )
93cv 1368 . . . . . 6  class  y
10 vz . . . . . . 7  setvar  z
1110cv 1368 . . . . . 6  class  z
12 cxmu 11088 . . . . . 6  class  xe
139, 11, 12co 6091 . . . . 5  class  ( y xe z )
142cv 1368 . . . . 5  class  x
1513, 14wceq 1369 . . . 4  wff  ( y xe z )  =  x
1615, 10, 4crio 6051 . . 3  class  ( iota_ z  e.  RR*  ( y xe z )  =  x )
172, 3, 4, 8, 16cmpt2 6093 . 2  class  ( x  e.  RR* ,  y  e.  ( RR  \  {
0 } )  |->  (
iota_ z  e.  RR*  (
y xe z )  =  x ) )
181, 17wceq 1369 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  26094
  Copyright terms: Public domain W3C validator