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 5649
Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5662) . (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 5648 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5083 . . . 4 class 𝑅
63csn 4155 . . . 4 class {𝑋}
75, 6cima 5087 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3559 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1480 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  5650  nfpred  5654  predpredss  5655  predss  5656  sspred  5657  dfpred2  5658  elpredim  5661  elpred  5662  elpredg  5663  predasetex  5664  dffr4  5665  predel  5666  predidm  5671  predin  5672  predun  5673  preddif  5674  predep  5675  pred0  5679  wfi  5682  frind  31494  csbpredg  32843
  Copyright terms: Public domain W3C validator