Theorem prtlem5

Description: Lemma for prter1 , prter2 , prter3 and prtex . (Contributed by Rodolfo Medina, 25-Sep-2010) (Proof shortened by Mario Carneiro, 11-Dec-2016)

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

Proof

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