Definition df-pred 6030

Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6043) . (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 6029	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5449	. . . 4 class ◡𝑅
6	3	csn 4478	. . . 4 class {𝑋}
7	5, 6	cima 5453	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3864	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1525	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6031  nfpred  6035  predpredss  6036  predss  6037  sspred  6038  dfpred2  6039  elpredim  6042  elpred  6043  elpredg  6044  predasetex  6045  dffr4  6046  predel  6047  predidm  6052  predin  6053  predun  6054  preddif  6055  predep  6056  pred0  6060  wfi  6063  frpoind  32691  frind  32696  csbpredg  34159