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

Theorem bj-ex 15199
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 1609 and 19.9ht 1652 or 19.23ht 1508). (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ex  |-  ( E. x ph  ->  ph )
Distinct variable group:    ph, x

Proof of Theorem bj-ex
StepHypRef Expression
1 ax-ie2 1505 . . 3  |-  ( A. x ( ph  ->  A. x ph )  -> 
( A. x (
ph  ->  ph )  <->  ( E. x ph  ->  ph ) ) )
2 ax-17 1537 . . 3  |-  ( ph  ->  A. x ph )
31, 2mpg 1462 . 2  |-  ( A. x ( ph  ->  ph )  <->  ( E. x ph  ->  ph ) )
4 id 19 . 2  |-  ( ph  ->  ph )
53, 4mpgbi 1463 1  |-  ( E. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wal 1362   E.wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-17 1537
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bj-d0clsepcl  15362  bj-inf2vnlem1  15407  bj-nn0sucALT  15415
  Copyright terms: Public domain W3C validator