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

Theorem bnj1317 28618
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 2355 . 2  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2hbxfreq 2469 1  |-  ( y  e.  A  ->  A. x  y  e.  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1545    = wceq 1647    e. wcel 1715   {cab 2352
This theorem is referenced by:  bnj1014  28756  bnj1145  28787  bnj1384  28826  bnj1398  28828  bnj1448  28841  bnj1450  28844  bnj1466  28847  bnj1463  28849  bnj1491  28851  bnj1497  28854  bnj1498  28855  bnj1520  28860  bnj1501  28861
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362
  Copyright terms: Public domain W3C validator