Theorem 2sb8e

Description: An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 . For a version requiring more disjoint variables, but fewer axioms, see 2sb8ef . (Contributed by Wolf Lammen, 2-Nov-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	2sb8e	$$⊢\exists x\exists y\phi \leftrightarrow \exists z\exists w\left[z/x\right]\left[w/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎw\phi$$
2	1	sb8e	$$⊢\exists y\phi \leftrightarrow \exists w\left[w/y\right]\phi$$
3	2	exbii	$$⊢\exists x\exists y\phi \leftrightarrow \exists x\exists w\left[w/y\right]\phi$$
4		excom	$$⊢\exists x\exists w\left[w/y\right]\phi \leftrightarrow \exists w\exists x\left[w/y\right]\phi$$
5	3 4	bitri	$$⊢\exists x\exists y\phi \leftrightarrow \exists w\exists x\left[w/y\right]\phi$$
6		nfv	$$⊢Ⅎz\phi$$
7	6	nfsb	$$⊢Ⅎz\left[w/y\right]\phi$$
8	7	sb8e	$$⊢\exists x\left[w/y\right]\phi \leftrightarrow \exists z\left[z/x\right]\left[w/y\right]\phi$$
9	8	exbii	$$⊢\exists w\exists x\left[w/y\right]\phi \leftrightarrow \exists w\exists z\left[z/x\right]\left[w/y\right]\phi$$
10		excom	$$⊢\exists w\exists z\left[z/x\right]\left[w/y\right]\phi \leftrightarrow \exists z\exists w\left[z/x\right]\left[w/y\right]\phi$$
11	5 9 10	3bitri	$$⊢\exists x\exists y\phi \leftrightarrow \exists z\exists w\left[z/x\right]\left[w/y\right]\phi$$