Theorem bj-ex 16126

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 1644 and 19.9ht 1687 or 19.23ht 1543). (Proof modification is discouraged.)

Assertion

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

Distinct variable group:   𝜑,𝑥

Proof of Theorem bj-ex

Step	Hyp	Ref	Expression
1		ax-ie2 1540	. . 3 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑)))
2		ax-17 1572	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1497	. 2 ⊢ (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑))
4		id 19	. 2 ⊢ (𝜑 → 𝜑)
5	3, 4	mpgbi 1498	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1393  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bj-d0clsepcl  16288  bj-inf2vnlem1  16333  bj-nn0sucALT  16341