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

Metamath Proof Explorer

Theorem dfpred2

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 8-Feb-2011)

		Ref	Expression
	Hypothesis	dfpred2.1	$⊢ X \in V$
	Assertion	dfpred2	$⊢ Pred (R, A, X) = A \cap \{y \| y R X\}$

Step	Hyp	Ref	Expression
1		dfpred2.1	$⊢ X \in V$
2		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
3		iniseg	$⊢ X \in V \to R^{-1} [\{X\}] = \{y \| y R X\}$
4	1 3	ax-mp	$⊢ R^{-1} [\{X\}] = \{y \| y R X\}$
5	4	ineq2i	$⊢ A \cap R^{-1} [\{X\}] = A \cap \{y \| y R X\}$
6	2 5	eqtri	$⊢ Pred (R, A, X) = A \cap \{y \| y R X\}$