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

Theorem r19.23v 2823
Description: Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
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 nfv 1672 . 2  |-  F/ x ps
21r19.23 2822 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( E. x  e.  A  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2705   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  ralxpxfr2d  3073  uniiunlem  3428  dfiin2g  4191  iunss  4199  ralxfr2d  4496  ssrel2  4917  reliun  4947  funimass4  5730  ralrnmpt2  6194  kmlem12  8318  fimaxre3  10267  gcdcllem1  13678  vdwmc2  14023  iunocv  17948  islindf4  18109  ovolgelb  20805  dyadmax  20920  itg2leub  21054  mptelee  22964  nmoubi  23995  nmopub  25135  nmfnleub  25152  sigaclcu2  26417  untuni  27207  dfpo2  27412  heibor1lem  28552  2reu4a  29859  ispsubsp2  32984  pmapglbx  33007
  Copyright terms: Public domain W3C validator