Definition df-pred 6206

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

This definition is referenced by:  predeq123  6207  nfpred  6211  csbpredg  6212  predpredss  6213  predss  6214  sspred  6215  dfpred2  6216  elpredgg  6219  predexg  6224  dffr4  6226  predel  6227  predidm  6233  predin  6234  predun  6235  preddif  6236  predep  6237  pred0  6242  dfse3  6243  predrelss  6244  predprc  6245  predres  6246  frpoind  6249  wfiOLD  6258  frind  9517