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 6305
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6322). (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 6304 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5676 . . . 4 class 𝑅
63csn 4629 . . . 4 class {𝑋}
75, 6cima 5680 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3944 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1533 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  6306  nfpred  6310  csbpredg  6311  predpredss  6312  predss  6313  sspred  6314  dfpred2  6315  elpredgg  6318  predexg  6323  dffr4  6325  predel  6326  predidm  6332  predin  6333  predun  6334  preddif  6335  predep  6336  pred0  6341  dfse3  6342  predrelss  6343  predprc  6344  predres  6345  frpoind  6348  wfiOLD  6357  frind  9773
  Copyright terms: Public domain W3C validator