Definition df-pred 6304

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

This definition is used by:  predeq123  6305  nfpred  6309  csbpredg  6310  predpredss  6311  predss  6312  sspred  6313  dfpred2  6314  elpredgg  6317  predexg  6322  dffr4  6323  predel  6324  predidm  6329  predin  6330  predun  6331  preddif  6332  predep  6333  pred0  6338  dfse3  6339  predrelss  6340  predprc  6341  predres  6342  frpoind  6345  frind  9757