Definition df-pred 6266

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

This definition is referenced by:  predeq123  6267  nfpred  6271  csbpredg  6272  predpredss  6273  predss  6274  sspred  6275  dfpred2  6276  elpredgg  6279  predexg  6284  dffr4  6285  predel  6286  predidm  6291  predin  6292  predun  6293  preddif  6294  predep  6295  pred0  6300  dfse3  6301  predrelss  6302  predprc  6303  predres  6304  frpoind  6307  frind  9674