Theorem bj-ex 13882

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 1592 and 19.9ht 1635 or 19.23ht 1491). (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 1488	. . 3 |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) ) )
2		ax-17 1520	. . 3 |- ( ph -> A. x ph )
3	1, 2	mpg 1445	. 2 |- ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) )
4		id 19	. 2 |- ( ph -> ph )
5	3, 4	mpgbi 1446	1 |- ( E. x ph -> ph )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1347   E.wex 1486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1443  ax-ie2 1488  ax-17 1520

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bj-d0clsepcl  14045  bj-inf2vnlem1  14090  bj-nn0sucALT  14098