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

Metamath Proof Explorer

Theorem elpred

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011) (Proof shortened by BJ, 16-Oct-2024)

		Ref	Expression
	Hypothesis	elpred.1	$⊢ Y \in V$
	Assertion	elpred	$⊢ X \in D \to (Y \in Pred (R, A, X) \leftrightarrow (Y \in A \land Y R X))$

Step	Hyp	Ref	Expression
1		elpred.1	$⊢ Y \in V$
2		elpredgg	$⊢ (X \in D \land Y \in V) \to (Y \in Pred (R, A, X) \leftrightarrow (Y \in A \land Y R X))$
3	1 2	mpan2	$⊢ X \in D \to (Y \in Pred (R, A, X) \leftrightarrow (Y \in A \land Y R X))$