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

Metamath Proof Explorer

Theorem predep

Description: The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	predep	$⊢ X \in B \to Pred (E, A, X) = A \cap X$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$⊢ Pred (E, A, X) = A \cap E^{-1} [\{X\}]$
2		relcnv	$⊢ Rel E^{-1}$
3		relimasn	$⊢ Rel E^{-1} \to E^{-1} [\{X\}] = \{y \| X E^{-1} y\}$
4	2 3	ax-mp	$⊢ E^{-1} [\{X\}] = \{y \| X E^{-1} y\}$
5		brcnvg	$⊢ (X \in B \land y \in V) \to (X E^{-1} y \leftrightarrow y E X)$
6	5	elvd	$⊢ X \in B \to (X E^{-1} y \leftrightarrow y E X)$
7		epelg	$⊢ X \in B \to (y E X \leftrightarrow y \in X)$
8	6 7	bitrd	$⊢ X \in B \to (X E^{-1} y \leftrightarrow y \in X)$
9	8	eqabcdv	$⊢ X \in B \to \{y \| X E^{-1} y\} = X$
10	4 9	eqtrid	$⊢ X \in B \to E^{-1} [\{X\}] = X$
11	10	ineq2d	$⊢ X \in B \to A \cap E^{-1} [\{X\}] = A \cap X$
12	1 11	eqtrid	$⊢ X \in B \to Pred (E, A, X) = A \cap X$