Definition df-pred 6292

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6309). (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 6291	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5651	. . . 4 class ◡𝑅
6	3	csn 4585	. . . 4 class {𝑋}
7	5, 6	cima 5655	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3906	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1563	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6293  nfpred  6297  csbpredg  6298  predpredss  6299  predss  6300  sspred  6301  dfpred2  6302  elpredgg  6305  predexg  6310  dffr4  6311  predel  6312  predidm  6317  predin  6318  predun  6319  preddif  6320  predep  6321  pred0  6326  dfse3  6327  predrelss  6328  predprc  6329  predres  6330  frpoind  6333  frind  9710