Definition df-pred 5718

Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5731) . (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 5717	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5142	. . . 4 class ◡𝑅
6	3	csn 4210	. . . 4 class {𝑋}
7	5, 6	cima 5146	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3606	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1523	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  5719  nfpred  5723  predpredss  5724  predss  5725  sspred  5726  dfpred2  5727  elpredim  5730  elpred  5731  elpredg  5732  predasetex  5733  dffr4  5734  predel  5735  predidm  5740  predin  5741  predun  5742  preddif  5743  predep  5744  pred0  5748  wfi  5751  frpoind  31865  frind  31868  csbpredg  33302