prtlem5

		Ref	Expression
	Assertion	prtlem5	$⊢ [s/ v] [r/ u] \exists x \in A (u \in x \land v \in x) \leftrightarrow \exists x \in A (r \in x \land s \in x)$

Step	Hyp	Ref	Expression
1		elequ1	$⊢ u = r \to (u \in x \leftrightarrow r \in x)$
2		elequ1	$⊢ v = s \to (v \in x \leftrightarrow s \in x)$
3	1 2	bi2anan9r	$⊢ (v = s \land u = r) \to ((u \in x \land v \in x) \leftrightarrow (r \in x \land s \in x))$
4	3	rexbidv	$⊢ (v = s \land u = r) \to (\exists x \in A (u \in x \land v \in x) \leftrightarrow \exists x \in A (r \in x \land s \in x))$
5	4	2sbievw	$⊢ [s/ v] [r/ u] \exists x \in A (u \in x \land v \in x) \leftrightarrow \exists x \in A (r \in x \land s \in x)$

Metamath Proof Explorer