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	|- ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ w ph
2		nfv	|- F/ z ph
3	1 2	2sb8ev	|- ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )
4		2sb6	|- ( [ z / x ] [ w / y ] ph <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
5	4	2exbii	|- ( E. z E. w [ z / x ] [ w / y ] ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
6	3 5	bitri	|- ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )