Definition df-pred 6140

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6153). (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 6139	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5535	. . . 4 class ◡𝑅
6	3	csn 4527	. . . 4 class {𝑋}
7	5, 6	cima 5539	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3852	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1543	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6141  nfpred  6145  predpredss  6146  predss  6147  sspred  6148  dfpred2  6149  elpredim  6152  elpred  6153  elpredg  6154  predasetex  6155  dffr4  6156  predel  6157  predidm  6162  predin  6163  predun  6164  preddif  6165  predep  6166  pred0  6171  frpoind  6174  wfi  6181  dfse3  33347  frind  33460  csbpredg  35183