This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 2sb8ef.1 
 |-  F/ w ph
2 2sb8ef.2 
 |-  F/ z ph
3 1 sb8ef 
 |-  ( 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 sb8ef 
 |-  ( 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 )