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	syl5bb	|- ( ph -> ( E. x E. y ps <-> E. y ps ) )