MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pred Structured version   Visualization version   GIF version

Definition df-pred 6321
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6338). (Contributed by Scott Fenton, 29-Jan-2011.)
Assertion
Ref Expression
df-pred Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))

Detailed syntax breakdown of Definition df-pred
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cX . . 3 class 𝑋
41, 2, 3cpred 6320 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5684 . . . 4 class 𝑅
63csn 4626 . . . 4 class {𝑋}
75, 6cima 5688 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3950 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1540 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  6322  nfpred  6326  csbpredg  6327  predpredss  6328  predss  6329  sspred  6330  dfpred2  6331  elpredgg  6334  predexg  6339  dffr4  6341  predel  6342  predidm  6347  predin  6348  predun  6349  preddif  6350  predep  6351  pred0  6356  dfse3  6357  predrelss  6358  predprc  6359  predres  6360  frpoind  6363  wfiOLD  6372  frind  9790
  Copyright terms: Public domain W3C validator