Theorem bj-ex 11618

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 1534 and 19.9ht 1577 or 19.23ht 1431). (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 1428	. . 3 |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) ) )
2		ax-17 1464	. . 3 |- ( ph -> A. x ph )
3	1, 2	mpg 1385	. 2 |- ( A. x ( ph -> ph ) <-> ( E. x ph -> ph ) )
4		id 19	. 2 |- ( ph -> ph )
5	3, 4	mpgbi 1386	1 |- ( E. x ph -> ph )

Syntax hints:   -> wi 4   <-> wb 103   A.wal 1287   E.wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1383  ax-ie2 1428  ax-17 1464

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bj-d0clsepcl  11775  bj-inf2vnlem1  11820  bj-nn0sucALT  11828