Definition df-pred

Description: Define the predecessor class of a binary relation. This is the class of all elements y of A such that y R X (see elpred ). (Contributed by Scott Fenton, 29-Jan-2011)

	Ref	Expression
Assertion	df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2		cX	⊢ 𝑋
3	1 0 2	cpred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 )
4	0	ccnv	⊢ ◡ 𝑅
5	2	csn	⊢ { 𝑋 }
6	4 5	cima	⊢ ( ◡ 𝑅 “ { 𝑋 } )
7	1 6	cin	⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
8	3 7	wceq	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )