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

Metamath Proof Explorer

Theorem predel

Description: Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011)

		Ref	Expression
	Assertion	predel	$⊢ Y \in Pred (R, A, X) \to Y \in A$

Step	Hyp	Ref	Expression
1		elinel1	$⊢ Y \in (A \cap R^{-1} [\{X\}]) \to Y \in A$
2		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
3	1 2	eleq2s	$⊢ Y \in Pred (R, A, X) \to Y \in A$