elpredgg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011) Generalize to closed form. (Revised by BJ, 16-Oct-2024)

		Ref	Expression
	Assertion	elpredgg	$⊢ (X \in V \land Y \in W) \to (Y \in Pred (R, A, X) \leftrightarrow (Y \in A \land Y R X))$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
2	1	elin2	$⊢ Y \in Pred (R, A, X) \leftrightarrow (Y \in A \land Y \in R^{-1} [\{X\}])$
3		elinisegg	$⊢ (X \in V \land Y \in W) \to (Y \in R^{-1} [\{X\}] \leftrightarrow Y R X)$
4	3	anbi2d	$⊢ (X \in V \land Y \in W) \to ((Y \in A \land Y \in R^{-1} [\{X\}]) \leftrightarrow (Y \in A \land Y R X))$
5	2 4	bitrid	$⊢ (X \in V \land Y \in W) \to (Y \in Pred (R, A, X) \leftrightarrow (Y \in A \land Y R X))$

Metamath Proof Explorer

Theorem elpredgg

Proof