Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-ex GIF version

Theorem bj-ex 13758
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 1591 and 19.9ht 1634 or 19.23ht 1490). (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ex (∃𝑥𝜑𝜑)
Distinct variable group:   𝜑,𝑥

Proof of Theorem bj-ex
StepHypRef Expression
1 ax-ie2 1487 . . 3 (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑)))
2 ax-17 1519 . . 3 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1444 . 2 (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑))
4 id 19 . 2 (𝜑𝜑)
53, 4mpgbi 1445 1 (∃𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1346  wex 1485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-17 1519
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bj-d0clsepcl  13922  bj-inf2vnlem1  13967  bj-nn0sucALT  13975
  Copyright terms: Public domain W3C validator