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

Theorem bnj937 29142
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 1676 . 2  |-  ( E. x ps  <->  ps )
31, 2sylib 189 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  bnj1265  29184  bnj1379  29202  bnj852  29292  bnj1148  29365  bnj1154  29368  bnj1189  29378  bnj1245  29383  bnj1286  29388  bnj1311  29393  bnj1371  29398  bnj1374  29400  bnj1498  29430  bnj1514  29432
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
  Copyright terms: Public domain W3C validator