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

Theorem r19.41v 2693
Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)
Assertion
Ref Expression
r19.41v  |-  ( E. 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.41v
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ps
21r19.41 2692 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wrex 2544
This theorem is referenced by:  r19.42v  2694  3reeanv  2708  reuind  2968  iuncom4  3912  dfiun2g  3935  iunxiun  3984  inuni  4173  reuxfrd  4559  xpiundi  4743  xpiundir  4744  imaco  5178  coiun  5182  abrexco  5766  imaiun  5771  isomin  5834  isoini  5835  oarec  6560  mapsnen  6938  genpass  8633  4sqlem12  13003  imasleval  13443  lsmspsn  15837  metrest  18070  nmoo0  21369  hhcmpl  21779  nmop0  22566  nmfn0  22567  reuxfr4d  23139  rexunirn  23140  r19.41vv  23163  nofulllem5  24360  elfuns  24454  axsegcon  24555  axeuclid  24591  prtlem11  26734  prter2  26749  prter3  26750  diophrex  26855  islshpat  29207  lshpsmreu  29299  islpln5  29724  islvol5  29768  cdlemftr3  30754  dvhb1dimN  31175  dib1dim  31355  mapdpglem3  31865  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator