Definition df-pred 6303

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

This definition is used by:  predeq123  6304  nfpred  6308  csbpredg  6309  predpredss  6310  predss  6311  sspred  6312  dfpred2  6313  elpredgg  6316  predexg  6321  dffr4  6322  predel  6323  predidm  6328  predin  6329  predun  6330  preddif  6331  predep  6332  pred0  6337  dfse3  6338  predrelss  6339  predprc  6340  predres  6341  frpoind  6344  frind  9736