Definition df-pred 6282

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6299). (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 6281	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5644	. . . 4 class ◡𝑅
6	3	csn 4581	. . . 4 class {𝑋}
7	5, 6	cima 5648	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3903	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1559	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6283  nfpred  6287  csbpredg  6288  predpredss  6289  predss  6290  sspred  6291  dfpred2  6292  elpredgg  6295  predexg  6300  dffr4  6301  predel  6302  predidm  6307  predin  6308  predun  6309  preddif  6310  predep  6311  pred0  6316  dfse3  6317  predrelss  6318  predprc  6319  predres  6320  frpoind  6323  frind  9703