Definition df-pred 6253

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

This definition is referenced by:  predeq123  6254  nfpred  6258  csbpredg  6259  predpredss  6260  predss  6261  sspred  6262  dfpred2  6263  elpredgg  6266  predexg  6271  dffr4  6272  predel  6273  predidm  6278  predin  6279  predun  6280  preddif  6281  predep  6282  pred0  6287  dfse3  6288  predrelss  6289  predprc  6290  predres  6291  frpoind  6294  frind  9665