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

Definition df-pred 24239
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 24248) . (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 24238 . 2  class  Pred ( R ,  A ,  X )
52ccnv 4704 . . . 4  class  `' R
63csn 3653 . . . 4  class  { X }
75, 6cima 4708 . . 3  class  ( `' R " { X } )
81, 7cin 3164 . 2  class  ( A  i^i  ( `' R " { X } ) )
94, 8wceq 1632 1  wff  Pred ( R ,  A ,  X )  =  ( A  i^i  ( `' R " { X } ) )
Colors of variables: wff set class
This definition is referenced by:  predeq1  24240  predeq2  24241  predeq3  24242  predpredss  24243  predss  24244  sspred  24245  dfpred2  24246  elpredim  24247  elpred  24248  elpredg  24249  predasetex  24251  dffr4  24253  predel  24254  predidm  24259  predin  24260  predun  24261  preddif  24262  predep  24263  pred0  24270  wfi  24278  frind  24314
  Copyright terms: Public domain W3C validator