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

Theorem bj-ex 9902
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 1489 and 19.9ht 1532 or 19.23ht 1386). (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 1383 . . 3  |-  ( A. x ( ph  ->  A. x ph )  -> 
( A. x (
ph  ->  ph )  <->  ( E. x ph  ->  ph ) ) )
2 ax-17 1419 . . 3  |-  ( ph  ->  A. x ph )
31, 2mpg 1340 . 2  |-  ( A. x ( ph  ->  ph )  <->  ( E. x ph  ->  ph ) )
4 id 19 . 2  |-  ( ph  ->  ph )
53, 4mpgbi 1341 1  |-  ( E. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98   A.wal 1241   E.wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1338  ax-ie2 1383  ax-17 1419
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bj-d0clsepcl  10049  bj-inf2vnlem1  10095  bj-nn0sucALT  10103
  Copyright terms: Public domain W3C validator