Definition df-pred 6290

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

This definition is referenced by:  predeq123  6291  nfpred  6295  csbpredg  6296  predpredss  6297  predss  6298  sspred  6299  dfpred2  6300  elpredgg  6303  predexg  6308  dffr4  6309  predel  6310  predidm  6315  predin  6316  predun  6317  preddif  6318  predep  6319  pred0  6324  dfse3  6325  predrelss  6326  predprc  6327  predres  6328  frpoind  6331  wfiOLD  6340  frind  9762