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

Theorem r19.23v 2937
Description: Restricted quantifier version of 19.23v 1761. Version of r19.23 2936 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 292 . . 3  |-  ( (
ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) )
21ralbii 2888 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  ( -.  ps  ->  -.  ph ) )
3 r19.21v 2862 . 2  |-  ( A. x  e.  A  ( -.  ps  ->  -.  ph )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph )
)
4 dfrex2 2908 . . . 4  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )
54imbi1i 325 . . 3  |-  ( ( E. x  e.  A  ph 
->  ps )  <->  ( -.  A. x  e.  A  -.  ph 
->  ps ) )
6 con1b 333 . . 3  |-  ( ( -.  A. x  e.  A  -.  ph  ->  ps )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph ) )
75, 6bitr2i 250 . 2  |-  ( ( -.  ps  ->  A. x  e.  A  -.  ph )  <->  ( E. x  e.  A  ph 
->  ps ) )
82, 3, 73bitri 271 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 184   A.wral 2807   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-ral 2812  df-rex 2813
This theorem is referenced by:  rexlimiv  2943  ralxpxfr2d  3224  uniiunlem  3584  dfiin2g  4365  iunss  4373  ralxfr2d  4672  ssrel2  5102  reliun  5132  funimass4  5924  ralrnmpt2  6416  kmlem12  8558  fimaxre3  10512  gcdcllem1  14160  vdwmc2  14508  iunocv  18838  islindf4  18999  ovolgelb  22016  dyadmax  22132  itg2leub  22266  mptelee  24324  nmoubi  25813  nmopub  26953  nmfnleub  26970  sigaclcu2  28281  untuni  29256  dfpo2  29359  heibor1lem  30467  2reu4a  32355  ispsubsp2  35571  pmapglbx  35594
  Copyright terms: Public domain W3C validator