Definition df-pred 6257

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

This definition is referenced by:  predeq123  6258  nfpred  6262  csbpredg  6263  predpredss  6264  predss  6265  sspred  6266  dfpred2  6267  elpredgg  6270  predexg  6275  dffr4  6276  predel  6277  predidm  6282  predin  6283  predun  6284  preddif  6285  predep  6286  pred0  6291  dfse3  6292  predrelss  6293  predprc  6294  predres  6295  frpoind  6298  frind  9663