Theorem bj-ex 15698

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 1621 and 19.9ht 1664 or 19.23ht 1520). (Proof modification is discouraged.)

Assertion

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

Distinct variable group:   𝜑,𝑥

Proof of Theorem bj-ex

Step	Hyp	Ref	Expression
1		ax-ie2 1517	. . 3 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑)))
2		ax-17 1549	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1474	. 2 ⊢ (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑))
4		id 19	. 2 ⊢ (𝜑 → 𝜑)
5	3, 4	mpgbi 1475	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371  ∃wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bj-d0clsepcl  15861  bj-inf2vnlem1  15906  bj-nn0sucALT  15914