Definition df-pred 6265

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6282). (Contributed by Scott Fenton, 29-Jan-2011.)

Assertion

Ref	Expression
df-pred	⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

Detailed syntax breakdown of Definition df-pred

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3		cX	. . 3 class 𝑋
4	1, 2, 3	cpred 6264	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5630	. . . 4 class ◡𝑅
6	3	csn 4567	. . . 4 class {𝑋}
7	5, 6	cima 5634	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3888	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1542	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6266  nfpred  6270  csbpredg  6271  predpredss  6272  predss  6273  sspred  6274  dfpred2  6275  elpredgg  6278  predexg  6283  dffr4  6284  predel  6285  predidm  6290  predin  6291  predun  6292  preddif  6293  predep  6294  pred0  6299  dfse3  6300  predrelss  6301  predprc  6302  predres  6303  frpoind  6306  frind  9674