Definition df-pred 6259

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

This definition is referenced by:  predeq123  6260  nfpred  6264  csbpredg  6265  predpredss  6266  predss  6267  sspred  6268  dfpred2  6269  elpredgg  6272  predexg  6277  dffr4  6278  predel  6279  predidm  6284  predin  6285  predun  6286  preddif  6287  predep  6288  pred0  6293  dfse3  6294  predrelss  6295  predprc  6296  predres  6297  frpoind  6300  frind  9672