Definition df-pred 6191

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6208). (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 6190	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5579	. . . 4 class ◡𝑅
6	3	csn 4558	. . . 4 class {𝑋}
7	5, 6	cima 5583	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3882	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1539	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6192  nfpred  6196  csbpredg  6197  predpredss  6198  predss  6199  sspred  6200  dfpred2  6201  elpredgg  6204  predexg  6209  dffr4  6211  predel  6212  predidm  6218  predin  6219  predun  6220  preddif  6221  predep  6222  pred0  6227  frpoind  6230  wfiOLD  6239  frind  9439  dfse3  33580