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

Theorem r19.41v 2655
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 1629 . 2  |-  F/ x ps
21r19.41 2654 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 2510
This theorem is referenced by:  r19.42v  2656  3reeanv  2670  reuind  2903  iuncom4  3810  dfiun2g  3833  iunxiun  3882  inuni  4071  reuxfrd  4450  xpiundi  4650  xpiundir  4651  imaco  5084  coiun  5088  abrexco  5618  imaiun  5623  isomin  5686  isoini  5687  oarec  6446  mapsnen  6823  genpass  8513  4sqlem12  12877  imasleval  13317  lsmspsn  15672  metrest  17902  nmoo0  21199  hhcmpl  21609  nmop0  22396  nmfn0  22397  axfelem18  23531  axsegcon  23729  axeuclid  23765  prtlem11  25900  prter2  25915  prter3  25916  diophrex  26021  islshpat  28111  lshpsmreu  28203  islpln5  28628  islvol5  28672  cdlemftr3  29658  dvhb1dimN  30079  dib1dim  30259  mapdpglem3  30769  hdmapglem7a  31024
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-rex 2514
  Copyright terms: Public domain W3C validator