Definition df-pred 6277

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

This definition is referenced by:  predeq123  6278  nfpred  6282  csbpredg  6283  predpredss  6284  predss  6285  sspred  6286  dfpred2  6287  elpredgg  6290  predexg  6295  dffr4  6296  predel  6297  predidm  6302  predin  6303  predun  6304  preddif  6305  predep  6306  pred0  6311  dfse3  6312  predrelss  6313  predprc  6314  predres  6315  frpoind  6318  frind  9710