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

Theorem r19.23v 2905
Description: Restricted quantifier version of 19.23v 1807. Version of r19.23 2904 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 293 . . 3  |-  ( (
ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) )
21ralbii 2856 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  ( -.  ps  ->  -.  ph ) )
3 r19.21v 2830 . 2  |-  ( A. x  e.  A  ( -.  ps  ->  -.  ph )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph )
)
4 dfrex2 2876 . . . 4  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )
54imbi1i 326 . . 3  |-  ( ( E. x  e.  A  ph 
->  ps )  <->  ( -.  A. x  e.  A  -.  ph 
->  ps ) )
6 con1b 334 . . 3  |-  ( ( -.  A. x  e.  A  -.  ph  ->  ps )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph ) )
75, 6bitr2i 253 . 2  |-  ( ( -.  ps  ->  A. x  e.  A  -.  ph )  <->  ( E. x  e.  A  ph 
->  ps ) )
82, 3, 73bitri 274 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 187   A.wral 2775   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781
This theorem is referenced by:  rexlimiv  2911  ralxpxfr2d  3196  uniiunlem  3549  dfiin2g  4329  iunss  4337  ralxfr2d  4633  ssrel2  4940  reliun  4969  funimass4  5928  ralrnmpt2  6421  kmlem12  8591  fimaxre3  10553  gcdcllem1  14460  vdwmc2  14916  iunocv  19230  islindf4  19382  ovolgelb  22419  dyadmax  22542  itg2leub  22678  mptelee  24911  nmoubi  26398  nmopub  27546  nmfnleub  27563  sigaclcu2  28937  untuni  30331  dfpo2  30389  heibor1lem  32054  ispsubsp2  33229  pmapglbx  33252  2reu4a  38322
  Copyright terms: Public domain W3C validator