Definition df-pred 6301

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6318). (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 6300	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5676	. . . 4 class ◡𝑅
6	3	csn 4629	. . . 4 class {𝑋}
7	5, 6	cima 5680	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3948	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1542	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6302  nfpred  6306  csbpredg  6307  predpredss  6308  predss  6309  sspred  6310  dfpred2  6311  elpredgg  6314  predexg  6319  dffr4  6321  predel  6322  predidm  6328  predin  6329  predun  6330  preddif  6331  predep  6332  pred0  6337  dfse3  6338  predrelss  6339  predprc  6340  predres  6341  frpoind  6344  wfiOLD  6353  frind  9745