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

Theorem r19.41v 2694
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 1606 . 2  |-  F/ x ps
21r19.41 2693 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wrex 2545
This theorem is referenced by:  r19.42v  2695  3reeanv  2709  reuind  2969  iuncom4  3913  dfiun2g  3936  iunxiun  3985  inuni  4176  reuxfrd  4558  xpiundi  4742  xpiundir  4743  imaco  5176  coiun  5180  abrexco  5727  imaiun  5732  isomin  5795  isoini  5796  oarec  6555  mapsnen  6933  genpass  8628  4sqlem12  12997  imasleval  13437  lsmspsn  15831  metrest  18064  nmoo0  21361  hhcmpl  21771  nmop0  22558  nmfn0  22559  axfelem18  23764  axsegcon  23962  axeuclid  23998  prtlem11  26133  prter2  26148  prter3  26149  diophrex  26254  islshpat  28474  lshpsmreu  28566  islpln5  28991  islvol5  29035  cdlemftr3  30021  dvhb1dimN  30442  dib1dim  30622  mapdpglem3  31132  hdmapglem7a  31387
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533  df-rex 2550
  Copyright terms: Public domain W3C validator