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 6200
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6217). (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 6199 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5588 . . . 4 class 𝑅
63csn 4567 . . . 4 class {𝑋}
75, 6cima 5592 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3891 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1542 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  6201  nfpred  6205  csbpredg  6206  predpredss  6207  predss  6208  sspred  6209  dfpred2  6210  elpredgg  6213  predexg  6218  dffr4  6220  predel  6221  predidm  6227  predin  6228  predun  6229  preddif  6230  predep  6231  pred0  6236  dfse3  6237  predrelss  6238  predprc  6239  predres  6240  frpoind  6243  wfiOLD  6252  frind  9501
  Copyright terms: Public domain W3C validator