Theorem 2sb8ef

Description: An equivalent expression for double existence. Version of 2sb8e with more disjoint variable conditions, not requiring ax-13 . (Contributed by Wolf Lammen, 28-Jan-2023)

	Ref	Expression
Hypotheses	2sb8ef.1	$$⊢Ⅎw\phi$$
	2sb8ef.2	$$⊢Ⅎz\phi$$
Assertion	2sb8ef	$$⊢\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		2sb8ef.1	$$⊢Ⅎw\phi$$
2		2sb8ef.2	$$⊢Ⅎz\phi$$
3	1	sb8ef	$$⊢\exists y\phi \leftrightarrow \exists w\left[w/y\right]\phi$$
4	3	exbii	$$⊢\exists x\exists y\phi \leftrightarrow \exists x\exists w\left[w/y\right]\phi$$
5		excom	$$⊢\exists x\exists w\left[w/y\right]\phi \leftrightarrow \exists w\exists x\left[w/y\right]\phi$$
6	4 5	bitri	$$⊢\exists x\exists y\phi \leftrightarrow \exists w\exists x\left[w/y\right]\phi$$
7	2	nfsbv	$$⊢Ⅎz\left[w/y\right]\phi$$
8	7	sb8ef	$$⊢\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	6 9 10	3bitri	$$⊢\exists x\exists y\phi \leftrightarrow \exists z\exists w\left[z/x\right]\left[w/y\right]\phi$$