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

Theorem bj-ex 13074
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 1577 and 19.9ht 1620 or 19.23ht 1473). (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 1470 . . 3  |-  ( A. x ( ph  ->  A. x ph )  -> 
( A. x (
ph  ->  ph )  <->  ( E. x ph  ->  ph ) ) )
2 ax-17 1506 . . 3  |-  ( ph  ->  A. x ph )
31, 2mpg 1427 . 2  |-  ( A. x ( ph  ->  ph )  <->  ( E. x ph  ->  ph ) )
4 id 19 . 2  |-  ( ph  ->  ph )
53, 4mpgbi 1428 1  |-  ( E. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1329   E.wex 1468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-17 1506
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bj-d0clsepcl  13228  bj-inf2vnlem1  13273  bj-nn0sucALT  13281
  Copyright terms: Public domain W3C validator