Definition df-pred 6302

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6319). (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 6301	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5660	. . . 4 class ◡𝑅
6	3	csn 4588	. . . 4 class {𝑋}
7	5, 6	cima 5664	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3903	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1568	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6303  nfpred  6307  csbpredg  6308  predpredss  6309  predss  6310  sspred  6311  dfpred2  6312  elpredgg  6315  predexg  6320  dffr4  6321  predel  6322  predidm  6327  predin  6328  predun  6329  preddif  6330  predep  6331  pred0  6336  dfse3  6337  predrelss  6338  predprc  6339  predres  6340  frpoind  6343  frind  9721