This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (R, A, X) = A \cap R^{-1} [\{X\}]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2		cX	$class X$
3	1 0 2	cpred	$class Pred (R, A, X)$
4	0	ccnv	$class R^{-1}$
5	2	csn	$class \{X\}$
6	4 5	cima	$class R^{-1} [\{X\}]$
7	1 6	cin	$class (A \cap R^{-1} [\{X\}])$
8	3 7	wceq	$wff Pred (R, A, X) = A \cap R^{-1} [\{X\}]$