Theorem 2exsb

Description: An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005) (Proof shortened by Wolf Lammen, 30-Sep-2018)

	Ref	Expression
Assertion	2exsb	$$⊢\exists x\exists y\phi \leftrightarrow \exists z\exists w\forall x\forall y\left(\left(x=z\wedge y=w\right)\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎw\phi$$
2		nfv	$$⊢Ⅎz\phi$$
3	1 2	2sb8ef	$$⊢\exists x\exists y\phi \leftrightarrow \exists z\exists w\left[z/x\right]\left[w/y\right]\phi$$
4		2sb6	$$⊢\left[z/x\right]\left[w/y\right]\phi \leftrightarrow \forall x\forall y\left(\left(x=z\wedge y=w\right)\to \phi \right)$$
5	4	2exbii	$$⊢\exists z\exists w\left[z/x\right]\left[w/y\right]\phi \leftrightarrow \exists z\exists w\forall x\forall y\left(\left(x=z\wedge y=w\right)\to \phi \right)$$
6	3 5	bitri	$$⊢\exists x\exists y\phi \leftrightarrow \exists z\exists w\forall x\forall y\left(\left(x=z\wedge y=w\right)\to \phi \right)$$