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

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

Proof of Theorem bj-ex
StepHypRef Expression
1 ax-ie2 1424 . . 3 (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑)))
2 ax-17 1460 . . 3 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1381 . 2 (∀𝑥(𝜑𝜑) ↔ (∃𝑥𝜑𝜑))
4 id 19 . 2 (𝜑𝜑)
53, 4mpgbi 1382 1 (∃𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1283  wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-17 1460
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bj-d0clsepcl  10878  bj-inf2vnlem1  10923  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator