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

Theorem bnj1317 28854
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypothesis
Ref Expression
bnj1317.1  |-  A  =  { x  |  ph }
Assertion
Ref Expression
bnj1317  |-  ( y  e.  A  ->  A. x  y  e.  A )
Distinct variable group:    x, y
Allowed substitution hints:    ph( x, y)    A( x, y)

Proof of Theorem bnj1317
StepHypRef Expression
1 bnj1317.1 . 2  |-  A  =  { x  |  ph }
2 hbab1 2272 . 2  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2hbxfreq 2386 1  |-  ( y  e.  A  ->  A. x  y  e.  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    = wceq 1623    e. wcel 1684   {cab 2269
This theorem is referenced by:  bnj1014  28992  bnj1145  29023  bnj1384  29062  bnj1398  29064  bnj1448  29077  bnj1450  29080  bnj1466  29083  bnj1463  29085  bnj1491  29087  bnj1497  29090  bnj1498  29091  bnj1520  29096  bnj1501  29097
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  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator