Theorem bj-ex 16790

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 1651 and 19.9ht 1694 or 19.23ht 1550). (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 1547	. . 3 |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) ) )
2		ax-17 1579	. . 3 |- ( ph -> A. x ph )
3	1, 2	mpg 1504	. 2 |- ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) )
4		id 19	. 2 |- ( ph -> ph )
5	3, 4	mpgbi 1505	1 |- ( E. x ph -> ph )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  bj-d0clsepcl  16951  bj-inf2vnlem1  16996  bj-nn0sucALT  17004