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

Theorem r19.23v 2943
Description: Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (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 2895 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x  e.  A  ( -.  ps  ->  -.  ph ) )
3 r19.21v 2869 . 2  |-  ( A. x  e.  A  ( -.  ps  ->  -.  ph )  <->  ( -.  ps  ->  A. x  e.  A  -.  ph )
)
4 dfrex2 2915 . . . 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 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  rexlimiv  2949  ralxpxfr2d  3228  uniiunlem  3588  dfiin2g  4358  iunss  4366  ralxfr2d  4663  ssrel2  5091  reliun  5121  funimass4  5916  ralrnmpt2  6399  kmlem12  8537  fimaxre3  10488  gcdcllem1  14001  vdwmc2  14349  iunocv  18476  islindf4  18637  ovolgelb  21623  dyadmax  21739  itg2leub  21873  mptelee  23871  nmoubi  25360  nmopub  26500  nmfnleub  26517  sigaclcu2  27757  untuni  28553  dfpo2  28758  heibor1lem  29906  2reu4a  31661  ispsubsp2  34542  pmapglbx  34565
  Copyright terms: Public domain W3C validator