Definition df-pred 6260

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

This definition is referenced by:  predeq123  6261  nfpred  6265  csbpredg  6266  predpredss  6267  predss  6268  sspred  6269  dfpred2  6270  elpredgg  6273  predexg  6278  dffr4  6279  predel  6280  predidm  6285  predin  6286  predun  6287  preddif  6288  predep  6289  pred0  6294  dfse3  6295  predrelss  6296  predprc  6297  predres  6298  frpoind  6301  frind  9666