Definition df-pred 6256

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

This definition is referenced by:  predeq123  6257  nfpred  6261  csbpredg  6262  predpredss  6263  predss  6264  sspred  6265  dfpred2  6266  elpredgg  6269  predexg  6274  dffr4  6275  predel  6276  predidm  6281  predin  6282  predun  6283  preddif  6284  predep  6285  pred0  6290  dfse3  6291  predrelss  6292  predprc  6293  predres  6294  frpoind  6297  frind  9653