Definition df-pred 6148

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

This definition is referenced by:  predeq123  6149  nfpred  6153  predpredss  6154  predss  6155  sspred  6156  dfpred2  6157  elpredim  6160  elpred  6161  elpredg  6162  predasetex  6163  dffr4  6164  predel  6165  predidm  6170  predin  6171  predun  6172  preddif  6173  predep  6174  pred0  6178  wfi  6181  frpoind  33080  frind  33085  csbpredg  34610