Definition df-pred 6267

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

This definition is referenced by:  predeq123  6268  nfpred  6272  csbpredg  6273  predpredss  6274  predss  6275  sspred  6276  dfpred2  6277  elpredgg  6280  predexg  6285  dffr4  6286  predel  6287  predidm  6292  predin  6293  predun  6294  preddif  6295  predep  6296  pred0  6301  dfse3  6302  predrelss  6303  predprc  6304  predres  6305  frpoind  6308  frind  9674