MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.3rzv Structured version   Unicode version

Theorem r19.3rzv 3910
Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.)
Assertion
Ref Expression
r19.3rzv  |-  ( A  =/=  (/)  ->  ( ph  <->  A. x  e.  A  ph ) )
Distinct variable groups:    x, A    ph, x

Proof of Theorem r19.3rzv
StepHypRef Expression
1 n0 3793 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 biimt 333 . . 3  |-  ( E. x  x  e.  A  ->  ( ph  <->  ( E. x  x  e.  A  ->  ph ) ) )
31, 2sylbi 195 . 2  |-  ( A  =/=  (/)  ->  ( ph  <->  ( E. x  x  e.  A  ->  ph ) ) )
4 df-ral 2809 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
5 19.23v 1765 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  <->  ( E. x  x  e.  A  ->  ph ) )
64, 5bitri 249 . 2  |-  ( A. x  e.  A  ph  <->  ( E. x  x  e.  A  ->  ph ) )
73, 6syl6bbr 263 1  |-  ( A  =/=  (/)  ->  ( ph  <->  A. x  e.  A  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1396   E.wex 1617    e. wcel 1823    =/= wne 2649   A.wral 2804   (/)c0 3783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-v 3108  df-dif 3464  df-nul 3784
This theorem is referenced by:  r19.9rzv  3911  r19.28zv  3912  r19.37zv  3913  r19.27zv  3917  iinconst  4325  cnvpo  5528  supicc  11671  coe1mul2lem1  18503  neipeltop  19797  utop3cls  20920  frgrareg  25319  frgraregord013  25320  rencldnfi  30994  cvgdvgrat  31435  ralnralall  32668
  Copyright terms: Public domain W3C validator