Definition df-pred 6274

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6291). (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 6273	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5637	. . . 4 class ◡𝑅
6	3	csn 4589	. . . 4 class {𝑋}
7	5, 6	cima 5641	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3913	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1540	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6275  nfpred  6279  csbpredg  6280  predpredss  6281  predss  6282  sspred  6283  dfpred2  6284  elpredgg  6287  predexg  6292  dffr4  6293  predel  6294  predidm  6299  predin  6300  predun  6301  preddif  6302  predep  6303  pred0  6308  dfse3  6309  predrelss  6310  predprc  6311  predres  6312  frpoind  6315  frind  9703