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

Theorem bj-ex 9217
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 1486 and 19.9ht 1529 or 19.23ht 1383). (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ex
Distinct variable group:   ,

Proof of Theorem bj-ex
StepHypRef Expression
1 ax-ie2 1380 . . 3
2 ax-17 1416 . . 3
31, 2mpg 1337 . 2
4 id 19 . 2
53, 4mpgbi 1338 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wal 1240  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380  ax-17 1416
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bj-d0clsepcl  9360  bj-inf2vnlem1  9400  bj-nn0sucALT  9408
  Copyright terms: Public domain W3C validator