Definition df-pred 6200

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

This definition is referenced by:  predeq123  6201  nfpred  6205  csbpredg  6206  predpredss  6207  predss  6208  sspred  6209  dfpred2  6210  elpredgg  6213  predexg  6218  dffr4  6220  predel  6221  predidm  6227  predin  6228  predun  6229  preddif  6230  predep  6231  pred0  6236  dfse3  6237  predrelss  6238  predprc  6239  predres  6240  frpoind  6243  wfiOLD  6252  frind  9501