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 5718
Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5731) . (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 5717 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5142 . . . 4 class 𝑅
63csn 4210 . . . 4 class {𝑋}
75, 6cima 5146 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3606 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1523 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  5719  nfpred  5723  predpredss  5724  predss  5725  sspred  5726  dfpred2  5727  elpredim  5730  elpred  5731  elpredg  5732  predasetex  5733  dffr4  5734  predel  5735  predidm  5740  predin  5741  predun  5742  preddif  5743  predep  5744  pred0  5748  wfi  5751  frpoind  31865  frind  31868  csbpredg  33302
  Copyright terms: Public domain W3C validator