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 6322
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6339). (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 6321 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5687 . . . 4 class 𝑅
63csn 4630 . . . 4 class {𝑋}
75, 6cima 5691 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3961 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1536 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  6323  nfpred  6327  csbpredg  6328  predpredss  6329  predss  6330  sspred  6331  dfpred2  6332  elpredgg  6335  predexg  6340  dffr4  6342  predel  6343  predidm  6348  predin  6349  predun  6350  preddif  6351  predep  6352  pred0  6357  dfse3  6358  predrelss  6359  predprc  6360  predres  6361  frpoind  6364  wfiOLD  6373  frind  9787
  Copyright terms: Public domain W3C validator