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	$$⊢\phi \to Ⅎx\psi$$
Assertion	19.9dev	$$⊢\phi \to \left(\exists x\exists y\psi \leftrightarrow \exists y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.9dev.1	$$⊢\phi \to Ⅎx\psi$$
2		excom	$$⊢\exists x\exists y\psi \leftrightarrow \exists y\exists x\psi$$
3		19.9t	$$⊢Ⅎx\psi \to \left(\exists x\psi \leftrightarrow \psi \right)$$
4	1 3	syl	$$⊢\phi \to \left(\exists x\psi \leftrightarrow \psi \right)$$
5	4	exbidv	$$⊢\phi \to \left(\exists y\exists x\psi \leftrightarrow \exists y\psi \right)$$
6	2 5	bitrid	$$⊢\phi \to \left(\exists x\exists y\psi \leftrightarrow \exists y\psi \right)$$