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	\|- ( x = y -> ( ph <-> ps ) )
	Assertion	19.8aw	\|- ( ph -> E. x ph )

Proof

Step	Hyp	Ref	Expression
1		19.8aw.1	\|- ( x = y -> ( ph <-> ps ) )
2		alnex	\|- ( A. x -. ph <-> -. E. x ph )
3	1	notbid	\|- ( x = y -> ( -. ph <-> -. ps ) )
4	3	spw	\|- ( A. x -. ph -> -. ph )
5	2 4	sylbir	\|- ( -. E. x ph -> -. ph )
6	5	con4i	\|- ( ph -> E. x ph )