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

Definition df-pred 25382
Description: Define the predecessor class of a relationship. This is the class of all elements  y of  A such that  y R X (see elpred 25391) . (Contributed by Scott Fenton, 29-Jan-2011.)
Assertion
Ref Expression
df-pred  |-  Pred ( R ,  A ,  X )  =  ( A  i^i  ( `' R " { X } ) )

Detailed syntax breakdown of Definition df-pred
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
3 cX . . 3  class  X
41, 2, 3cpred 25381 . 2  class  Pred ( R ,  A ,  X )
52ccnv 4836 . . . 4  class  `' R
63csn 3774 . . . 4  class  { X }
75, 6cima 4840 . . 3  class  ( `' R " { X } )
81, 7cin 3279 . 2  class  ( A  i^i  ( `' R " { X } ) )
94, 8wceq 1649 1  wff  Pred ( R ,  A ,  X )  =  ( A  i^i  ( `' R " { X } ) )
Colors of variables: wff set class
This definition is referenced by:  predeq1  25383  predeq2  25384  predeq3  25385  predpredss  25386  predss  25387  sspred  25388  dfpred2  25389  elpredim  25390  elpred  25391  elpredg  25392  predasetex  25394  dffr4  25396  predel  25397  predidm  25402  predin  25403  predun  25404  preddif  25405  predep  25406  pred0  25413  wfi  25421  frind  25457
  Copyright terms: Public domain W3C validator