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

Definition df-pred 23579
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 23588) . (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 23578 . 2  class  Pred ( R ,  A ,  X )
52ccnv 4688 . . . 4  class  `' R
63csn 3640 . . . 4  class  { X }
75, 6cima 4692 . . 3  class  ( `' R " { X } )
81, 7cin 3151 . 2  class  ( A  i^i  ( `' R " { X } ) )
94, 8wceq 1623 1  wff  Pred ( R ,  A ,  X )  =  ( A  i^i  ( `' R " { X } ) )
Colors of variables: wff set class
This definition is referenced by:  predeq1  23580  predeq2  23581  predeq3  23582  predpredss  23583  predss  23584  sspred  23585  dfpred2  23586  elpredim  23587  elpred  23588  elpredg  23589  predasetex  23591  dffr4  23593  predel  23594  predidm  23599  predin  23600  predun  23601  preddif  23602  predep  23603  pred0  23610  wfi  23618  frind  23654
  Copyright terms: Public domain W3C validator