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 5582
Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5595) . (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 5581 . 2 class Pred(𝑅, 𝐴, 𝑋)
52ccnv 5026 . . . 4 class 𝑅
63csn 4124 . . . 4 class {𝑋}
75, 6cima 5030 . . 3 class (𝑅 “ {𝑋})
81, 7cin 3538 . 2 class (𝐴 ∩ (𝑅 “ {𝑋}))
94, 8wceq 1474 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
Colors of variables: wff setvar class
This definition is referenced by:  predeq123  5583  nfpred  5587  predpredss  5588  predss  5589  sspred  5590  dfpred2  5591  elpredim  5594  elpred  5595  elpredg  5596  predasetex  5597  dffr4  5598  predel  5599  predidm  5604  predin  5605  predun  5606  preddif  5607  predep  5608  pred0  5612  wfi  5615  frind  30777  csbpredg  32131
  Copyright terms: Public domain W3C validator