Definition df-pred 6297

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6314). (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 6296	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5650	. . . 4 class ◡𝑅
6	3	csn 4584	. . . 4 class {𝑋}
7	5, 6	cima 5654	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3898	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1570	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is used by:  predeq123  6298  nfpred  6302  csbpredg  6303  predpredss  6304  predss  6305  sspred  6306  dfpred2  6307  elpredgg  6310  predexg  6315  dffr4  6316  predel  6317  predidm  6322  predin  6323  predun  6324  preddif  6325  predep  6326  pred0  6331  dfse3  6332  predrelss  6333  predprc  6334  predres  6335  frpoind  6338  frind  9738