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

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

Proof of Theorem bj-ex
StepHypRef Expression
1 ax-ie2 1504 . . 3 (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑)))
2 ax-17 1536 . . 3 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1461 . 2 (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑))
4 id 19 . 2 (𝜑𝜑)
53, 4mpgbi 1462 1 (∃𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wal 1361  wex 1502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1459  ax-ie2 1504  ax-17 1536
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bj-d0clsepcl  15060  bj-inf2vnlem1  15105  bj-nn0sucALT  15113
  Copyright terms: Public domain W3C validator