Theorem bj-ex 14897

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 1608 and 19.9ht 1651 or 19.23ht 1507). (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-ex	⊢ (∃𝑥𝜑 → 𝜑)

Distinct variable group:   𝜑,𝑥

Proof of Theorem bj-ex

Step	Hyp	Ref	Expression
1		ax-ie2 1504	. . 3 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑)))
2		ax-17 1536	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1461	. 2 ⊢ (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑))
4		id 19	. 2 ⊢ (𝜑 → 𝜑)
5	3, 4	mpgbi 1462	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1361  ∃wex 1502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1459  ax-ie2 1504  ax-17 1536

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bj-d0clsepcl  15060  bj-inf2vnlem1  15105  bj-nn0sucALT  15113