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

Definition df-pred 25432
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 25445) . (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 25431 . 2  class  Pred ( R ,  A ,  X )
52ccnv 4870 . . . 4  class  `' R
63csn 3807 . . . 4  class  { X }
75, 6cima 4874 . . 3  class  ( `' R " { X } )
81, 7cin 3312 . 2  class  ( A  i^i  ( `' R " { X } ) )
94, 8wceq 1652 1  wff  Pred ( R ,  A ,  X )  =  ( A  i^i  ( `' R " { X } ) )
Colors of variables: wff set class
This definition is referenced by:  predeq123  25433  nfpred  25437  predpredss  25438  predss  25439  sspred  25440  dfpred2  25441  elpredim  25444  elpred  25445  elpredg  25446  predasetex  25448  dffr4  25450  predel  25451  predidm  25456  predin  25457  predun  25458  preddif  25459  predep  25460  pred0  25467  wfi  25475  frind  25511
  Copyright terms: Public domain W3C validator