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

Theorem bnj1317 28899
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 2393 . 2  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2hbxfreq 2507 1  |-  ( y  e.  A  ->  A. x  y  e.  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546    = wceq 1649    e. wcel 1721   {cab 2390
This theorem is referenced by:  bnj1014  29037  bnj1145  29068  bnj1384  29107  bnj1398  29109  bnj1448  29122  bnj1450  29125  bnj1466  29128  bnj1463  29130  bnj1491  29132  bnj1497  29135  bnj1498  29136  bnj1520  29141  bnj1501  29142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator