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

Metamath Proof Explorer

Theorem 19.9dev

Description: 19.9d in the case of an existential quantifier, avoiding the ax-10 from nfex that would be used for the hypothesis of 19.9d , at the cost of an additional DV condition on y , ph . (Contributed by SN, 26-May-2024)

Ref Expression
Hypothesis 19.9dev.1 
|- ( ph -> F/ x ps )
Assertion 19.9dev 
|- ( ph -> ( E. x E. y ps <-> E. y ps ) )

Proof

Step Hyp Ref Expression
1 19.9dev.1 
 |-  ( ph -> F/ x ps )
2 excom 
 |-  ( E. x E. y ps <-> E. y E. x ps )
3 19.9t 
 |-  ( F/ x ps -> ( E. x ps <-> ps ) )
4 1 3 syl 
 |-  ( ph -> ( E. x ps <-> ps ) )
5 4 exbidv 
 |-  ( ph -> ( E. y E. x ps <-> E. y ps ) )
6 2 5 bitrid 
 |-  ( ph -> ( E. x E. y ps <-> E. y ps ) )