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	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	Assertion	19.9dev	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 𝜓 ↔ ∃ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.9dev.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜓 ↔ ∃ 𝑦 ∃ 𝑥 𝜓 )
3		19.9t	⊢ ( Ⅎ 𝑥 𝜓 → ( ∃ 𝑥 𝜓 ↔ 𝜓 ) )
4	1 3	syl	⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 ↔ 𝜓 ) )
5	4	exbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜓 ) )
6	2 5	bitrid	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 𝜓 ↔ ∃ 𝑦 𝜓 ) )