Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj937 Unicode version

Theorem bnj937 28803
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypothesis
Ref Expression
bnj937.1  |-  ( ph  ->  E. x ps )
Assertion
Ref Expression
bnj937  |-  ( ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem bnj937
StepHypRef Expression
1 bnj937.1 . 2  |-  ( ph  ->  E. x ps )
2 19.9v 1663 . 2  |-  ( E. x ps  <->  ps )
31, 2sylib 188 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  bnj1265  28845  bnj1379  28863  bnj852  28953  bnj1148  29026  bnj1154  29029  bnj1189  29039  bnj1245  29044  bnj1286  29049  bnj1311  29054  bnj1371  29059  bnj1374  29061  bnj1498  29091  bnj1514  29093
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator