Theorem bj-ex 14599

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 1598 and 19.9ht 1641 or 19.23ht 1497). (Proof modification is discouraged.)

Assertion

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

Distinct variable group:   𝜑,𝑥

Proof of Theorem bj-ex

Step	Hyp	Ref	Expression
1		ax-ie2 1494	. . 3 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑)))
2		ax-17 1526	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1451	. 2 ⊢ (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑))
4		id 19	. 2 ⊢ (𝜑 → 𝜑)
5	3, 4	mpgbi 1452	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bj-d0clsepcl  14762  bj-inf2vnlem1  14807  bj-nn0sucALT  14815