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

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
StepHypRef Expression
1 ax-ie2 1453 . . 3 (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑)))
2 ax-17 1489 . . 3 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1410 . 2 (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑))
4 id 19 . 2 (𝜑𝜑)
53, 4mpgbi 1411 1 (∃𝑥𝜑𝜑)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator