Theorem bj-ex 12662

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 1560 and 19.9ht 1603 or 19.23ht 1456). (Proof modification is discouraged.)

Assertion

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

Distinct variable group:   𝜑,𝑥

Proof of Theorem bj-ex

Step	Hyp	Ref	Expression
1		ax-ie2 1453	. . 3 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑)))
2		ax-17 1489	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1410	. 2 ⊢ (∀𝑥(𝜑 → 𝜑) ↔ (∃𝑥𝜑 → 𝜑))
4		id 19	. 2 ⊢ (𝜑 → 𝜑)
5	3, 4	mpgbi 1411	1 ⊢ (∃𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1312  ∃wex 1451

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1408  ax-ie2 1453  ax-17 1489

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bj-d0clsepcl  12815  bj-inf2vnlem1  12860  bj-nn0sucALT  12868