Definition df-pred 5900

Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5913) . (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 5899	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5317	. . . 4 class ◡𝑅
6	3	csn 4377	. . . 4 class {𝑋}
7	5, 6	cima 5321	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3775	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1637	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  5901  nfpred  5905  predpredss  5906  predss  5907  sspred  5908  dfpred2  5909  elpredim  5912  elpred  5913  elpredg  5914  predasetex  5915  dffr4  5916  predel  5917  predidm  5922  predin  5923  predun  5924  preddif  5925  predep  5926  pred0  5930  wfi  5933  frpoind  32066  frind  32069  csbpredg  33491