Definition df-pred 6322

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

This definition is used by:  predeq123  6323  nfpred  6327  csbpredg  6328  predpredss  6329  predss  6330  sspred  6331  dfpred2  6332  elpredgg  6335  predexg  6340  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  frind  9781