Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ub Structured version   Unicode version

Definition df-ub 30635
Description: Define the upper bound relationship functor. See brub 30714 for value. (Contributed by Scott Fenton, 3-May-2018.)
Assertion
Ref Expression
df-ub  |- UB R  =  ( ( _V  X.  _V )  \  (
( _V  \  R
)  o.  `'  _E  ) )

Detailed syntax breakdown of Definition df-ub
StepHypRef Expression
1 cR . . 3  class  R
21cub 30611 . 2  class UB R
3 cvv 3081 . . . 4  class  _V
43, 3cxp 4848 . . 3  class  ( _V 
X.  _V )
53, 1cdif 3433 . . . 4  class  ( _V 
\  R )
6 cep 4759 . . . . 5  class  _E
76ccnv 4849 . . . 4  class  `'  _E
85, 7ccom 4854 . . 3  class  ( ( _V  \  R )  o.  `'  _E  )
94, 8cdif 3433 . 2  class  ( ( _V  X.  _V )  \  ( ( _V 
\  R )  o.  `'  _E  ) )
102, 9wceq 1437 1  wff UB R  =  ( ( _V  X.  _V )  \  (
( _V  \  R
)  o.  `'  _E  ) )
Colors of variables: wff setvar class
This definition is referenced by:  brub  30714
  Copyright terms: Public domain W3C validator