Definition df-pred 6299

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

This definition is referenced by:  predeq123  6300  nfpred  6304  csbpredg  6305  predpredss  6306  predss  6307  sspred  6308  dfpred2  6309  elpredgg  6312  predexg  6317  dffr4  6319  predel  6320  predidm  6326  predin  6327  predun  6328  preddif  6329  predep  6330  pred0  6335  dfse3  6336  predrelss  6337  predprc  6338  predres  6339  frpoind  6342  wfiOLD  6351  frind  9765