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

Metamath Proof Explorer

Theorem 19.8aw

Description: If a formula is true, then it is true for at least one instance. This is to 19.8a what spw is to sp . (Contributed by SN, 26-Sep-2024)

		Ref	Expression
	Hypothesis	19.8aw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	19.8aw	⊢ ( 𝜑 → ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		19.8aw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
3	1	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
4	3	spw	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 )
5	2 4	sylbir	⊢ ( ¬ ∃ 𝑥 𝜑 → ¬ 𝜑 )
6	5	con4i	⊢ ( 𝜑 → ∃ 𝑥 𝜑 )