Definition df-pred 6298

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

This definition is referenced by:  predeq123  6299  nfpred  6303  csbpredg  6304  predpredss  6305  predss  6306  sspred  6307  dfpred2  6308  elpredgg  6311  predexg  6316  dffr4  6318  predel  6319  predidm  6325  predin  6326  predun  6327  preddif  6328  predep  6329  pred0  6334  dfse3  6335  predrelss  6336  predprc  6337  predres  6338  frpoind  6341  wfiOLD  6350  frind  9742