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 5900
Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5913) . (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 5899 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5317 . . . 4 class 𝑅
63csn 4377 . . . 4 class {𝑋}
75, 6cima 5321 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3775 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1637 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  5901  nfpred  5905  predpredss  5906  predss  5907  sspred  5908  dfpred2  5909  elpredim  5912  elpred  5913  elpredg  5914  predasetex  5915  dffr4  5916  predel  5917  predidm  5922  predin  5923  predun  5924  preddif  5925  predep  5926  pred0  5930  wfi  5933  frpoind  32066  frind  32069  csbpredg  33491
  Copyright terms: Public domain W3C validator