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

Theorem bnj937 28314
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 1655 . 2  |-  ( E. x ps  <->  ps )
31, 2sylib 188 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1532
This theorem is referenced by:  bnj1265  28356  bnj1379  28374  bnj852  28464  bnj1148  28537  bnj1154  28540  bnj1189  28550  bnj1245  28555  bnj1286  28560  bnj1311  28565  bnj1371  28570  bnj1374  28572  bnj1498  28602  bnj1514  28604
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533
  Copyright terms: Public domain W3C validator