Definition df-pred 5649

Description: Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5662) . (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 5648	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5083	. . . 4 class ◡𝑅
6	3	csn 4155	. . . 4 class {𝑋}
7	5, 6	cima 5087	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3559	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1480	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  5650  nfpred  5654  predpredss  5655  predss  5656  sspred  5657  dfpred2  5658  elpredim  5661  elpred  5662  elpredg  5663  predasetex  5664  dffr4  5665  predel  5666  predidm  5671  predin  5672  predun  5673  preddif  5674  predep  5675  pred0  5679  wfi  5682  frind  31494  csbpredg  32843