Definition df-pred 6244

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6261). (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 6243	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5613	. . . 4 class ◡𝑅
6	3	csn 4574	. . . 4 class {𝑋}
7	5, 6	cima 5617	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3899	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1541	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6245  nfpred  6249  csbpredg  6250  predpredss  6251  predss  6252  sspred  6253  dfpred2  6254  elpredgg  6257  predexg  6262  dffr4  6263  predel  6264  predidm  6269  predin  6270  predun  6271  preddif  6272  predep  6273  pred0  6278  dfse3  6279  predrelss  6280  predprc  6281  predres  6282  frpoind  6285  frind  9635