Theorem 2sb8ev

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	2sb8ev.1	|- F/ w ph
	2sb8ev.2	|- F/ z ph
Assertion	2sb8ev	|- ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		2sb8ev.1	|- F/ w ph
2		2sb8ev.2	|- F/ z ph
3	1	sb8ev	|- ( E. y ph <-> E. w [ w / y ] ph )
4	3	exbii	|- ( E. x E. y ph <-> E. x E. w [ w / y ] ph )
5		excom	|- ( E. x E. w [ w / y ] ph <-> E. w E. x [ w / y ] ph )
6	4 5	bitri	|- ( E. x E. y ph <-> E. w E. x [ w / y ] ph )
7	2	nfsbv	|- F/ z [ w / y ] ph
8	7	sb8ev	|- ( E. x [ w / y ] ph <-> E. z [ z / x ] [ w / y ] ph )
9	8	exbii	|- ( E. w E. x [ w / y ] ph <-> E. w E. z [ z / x ] [ w / y ] ph )
10		excom	|- ( E. w E. z [ z / x ] [ w / y ] ph <-> E. z E. w [ z / x ] [ w / y ] ph )
11	6 9 10	3bitri	|- ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )