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 6120
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6133) . (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 6119 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5522 . . . 4 class 𝑅
63csn 4528 . . . 4 class {𝑋}
75, 6cima 5526 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3883 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1538 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  6121  nfpred  6125  predpredss  6126  predss  6127  sspred  6128  dfpred2  6129  elpredim  6132  elpred  6133  elpredg  6134  predasetex  6135  dffr4  6136  predel  6137  predidm  6142  predin  6143  predun  6144  preddif  6145  predep  6146  pred0  6150  wfi  6153  frpoind  33188  frind  33193  csbpredg  34738
  Copyright terms: Public domain W3C validator