Theorem bj-ex 16480

Description: Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1647 and 19.9ht 1690 or 19.23ht 1546). (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-ex	|- ( E. x ph -> ph )

Distinct variable group:   ph, x

Proof of Theorem bj-ex

Step	Hyp	Ref	Expression
1		ax-ie2 1543	. . 3 |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) ) )
2		ax-17 1575	. . 3 |- ( ph -> A. x ph )
3	1, 2	mpg 1500	. 2 |- ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) )
4		id 19	. 2 |- ( ph -> ph )
5	3, 4	mpgbi 1501	1 |- ( E. x ph -> ph )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1396   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bj-d0clsepcl  16641  bj-inf2vnlem1  16686  bj-nn0sucALT  16694