Definition df-pred 6309

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

This definition is used by:  predeq123  6310  nfpred  6314  csbpredg  6315  predpredss  6316  predss  6317  sspred  6318  dfpred2  6319  elpredgg  6322  predexg  6327  dffr4  6328  predel  6329  predidm  6334  predin  6335  predun  6336  preddif  6337  predep  6338  pred0  6343  dfse3  6344  predrelss  6345  predprc  6346  predres  6347  frpoind  6350  frind  9732