Definition df-pred 6321

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

This definition is referenced by:  predeq123  6322  nfpred  6326  csbpredg  6327  predpredss  6328  predss  6329  sspred  6330  dfpred2  6331  elpredgg  6334  predexg  6339  dffr4  6341  predel  6342  predidm  6347  predin  6348  predun  6349  preddif  6350  predep  6351  pred0  6356  dfse3  6357  predrelss  6358  predprc  6359  predres  6360  frpoind  6363  wfiOLD  6372  frind  9790