MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.23v Structured version   Visualization version   Unicode version

Theorem r19.23v 2879
Description: Restricted quantifier version of 19.23v 1829. Version of r19.23 2878 with a dv condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
Assertion
Ref Expression
r19.23v  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem r19.23v
StepHypRef Expression
1 con34b 298 . . 3  |-  ( (
ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) )
21ralbii 2831 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  ( -.  ps  ->  -.  ph ) )
3 r19.21v 2805 . 2  |-  ( A. x  e.  A  ( -.  ps  ->  -.  ph )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph )
)
4 dfrex2 2850 . . . 4  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )
54imbi1i 331 . . 3  |-  ( ( E. x  e.  A  ph 
->  ps )  <->  ( -.  A. x  e.  A  -.  ph 
->  ps ) )
6 con1b 339 . . 3  |-  ( ( -.  A. x  e.  A  -.  ph  ->  ps )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph ) )
75, 6bitr2i 258 . 2  |-  ( ( -.  ps  ->  A. x  e.  A  -.  ph )  <->  ( E. x  e.  A  ph 
->  ps ) )
82, 3, 73bitri 279 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189   A.wral 2749   E.wrex 2750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755
This theorem is referenced by:  rexlimiv  2885  ralxpxfr2d  3176  uniiunlem  3529  dfiin2g  4325  iunss  4333  ralxfr2d  4630  ssrel2  4944  reliun  4973  funimass4  5939  ralrnmpt2  6438  kmlem12  8617  fimaxre3  10581  gcdcllem1  14522  vdwmc2  14978  iunocv  19293  islindf4  19445  ovolgelb  22482  dyadmax  22605  itg2leub  22741  mptelee  24974  nmoubi  26462  nmopub  27610  nmfnleub  27627  sigaclcu2  28991  untuni  30385  dfpo2  30444  heibor1lem  32186  ispsubsp2  33356  pmapglbx  33379  2reu4a  38648
  Copyright terms: Public domain W3C validator