bnj1148

Description: Property of _pred . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj1148	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \in V$

Step	Hyp	Ref	Expression
1		elisset	$⊢ X \in A \to \exists x x = X$
2	1	adantl	$⊢ (R FrSe A \land X \in A) \to \exists x x = X$
3		bnj93	$⊢ (R FrSe A \land x \in A) \to pred (x, A, R) \in V$
4		eleq1	$⊢ x = X \to (x \in A \leftrightarrow X \in A)$
5	4	anbi2d	$⊢ x = X \to ((R FrSe A \land x \in A) \leftrightarrow (R FrSe A \land X \in A))$
6		bnj602	$⊢ x = X \to pred (x, A, R) = pred (X, A, R)$
7	6	eleq1d	$⊢ x = X \to (pred (x, A, R) \in V \leftrightarrow pred (X, A, R) \in V)$
8	5 7	imbi12d	$⊢ x = X \to (((R FrSe A \land x \in A) \to pred (x, A, R) \in V) \leftrightarrow ((R FrSe A \land X \in A) \to pred (X, A, R) \in V))$
9	3 8	mpbii	$⊢ x = X \to ((R FrSe A \land X \in A) \to pred (X, A, R) \in V)$
10	2 9	bnj593	$⊢ (R FrSe A \land X \in A) \to \exists x ((R FrSe A \land X \in A) \to pred (X, A, R) \in V)$
11	10	bnj937	$⊢ (R FrSe A \land X \in A) \to ((R FrSe A \land X \in A) \to pred (X, A, R) \in V)$
12	11	pm2.43i	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \in V$

Metamath Proof Explorer