Definition df-pred 6332

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6349). (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 6331	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5699	. . . 4 class ◡𝑅
6	3	csn 4648	. . . 4 class {𝑋}
7	5, 6	cima 5703	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3975	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1537	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6333  nfpred  6337  csbpredg  6338  predpredss  6339  predss  6340  sspred  6341  dfpred2  6342  elpredgg  6345  predexg  6350  dffr4  6352  predel  6353  predidm  6358  predin  6359  predun  6360  preddif  6361  predep  6362  pred0  6367  dfse3  6368  predrelss  6369  predprc  6370  predres  6371  frpoind  6374  wfiOLD  6383  frind  9819