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 5839
Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5852) . (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 5838 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5263 . . . 4 class 𝑅
63csn 4319 . . . 4 class {𝑋}
75, 6cima 5267 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3712 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1630 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  5840  nfpred  5844  predpredss  5845  predss  5846  sspred  5847  dfpred2  5848  elpredim  5851  elpred  5852  elpredg  5853  predasetex  5854  dffr4  5855  predel  5856  predidm  5861  predin  5862  predun  5863  preddif  5864  predep  5865  pred0  5869  wfi  5872  frpoind  32044  frind  32047  csbpredg  33481
  Copyright terms: Public domain W3C validator