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 5597
Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5610) . (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 5596 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5037 . . . 4 class 𝑅
63csn 4125 . . . 4 class {𝑋}
75, 6cima 5041 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3539 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1475 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  5598  nfpred  5602  predpredss  5603  predss  5604  sspred  5605  dfpred2  5606  elpredim  5609  elpred  5610  elpredg  5611  predasetex  5612  dffr4  5613  predel  5614  predidm  5619  predin  5620  predun  5621  preddif  5622  predep  5623  pred0  5627  wfi  5630  frind  30984  csbpredg  32348
  Copyright terms: Public domain W3C validator