Definition df-pred 6307

Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6324). (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 6306	. 2 class Pred(𝑅, 𝐴, 𝑋)
5	2	ccnv 5677	. . . 4 class ◡𝑅
6	3	csn 4630	. . . 4 class {𝑋}
7	5, 6	cima 5681	. . 3 class (◡𝑅 “ {𝑋})
8	1, 7	cin 3943	. 2 class (𝐴 ∩ (◡𝑅 “ {𝑋}))
9	4, 8	wceq 1533	1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))

This definition is referenced by:  predeq123  6308  nfpred  6312  csbpredg  6313  predpredss  6314  predss  6315  sspred  6316  dfpred2  6317  elpredgg  6320  predexg  6325  dffr4  6327  predel  6328  predidm  6334  predin  6335  predun  6336  preddif  6337  predep  6338  pred0  6343  dfse3  6344  predrelss  6345  predprc  6346  predres  6347  frpoind  6350  wfiOLD  6359  frind  9775