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 6307
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6324). (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 6306 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5677 . . . 4 class 𝑅
63csn 4630 . . . 4 class {𝑋}
75, 6cima 5681 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3943 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1533 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  6308  nfpred  6312  csbpredg  6313  predpredss  6314  predss  6315  sspred  6316  dfpred2  6317  elpredgg  6320  predexg  6325  dffr4  6327  predel  6328  predidm  6334  predin  6335  predun  6336  preddif  6337  predep  6338  pred0  6343  dfse3  6344  predrelss  6345  predprc  6346  predres  6347  frpoind  6350  wfiOLD  6359  frind  9775
  Copyright terms: Public domain W3C validator