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

Theorem r19.41v 2668
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 2667 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 2519
This theorem is referenced by:  r19.42v  2669  3reeanv  2683  reuind  2943  iuncom4  3886  dfiun2g  3909  iunxiun  3958  inuni  4149  reuxfrd  4531  xpiundi  4731  xpiundir  4732  imaco  5165  coiun  5169  abrexco  5700  imaiun  5705  isomin  5768  isoini  5769  oarec  6528  mapsnen  6906  genpass  8601  4sqlem12  12965  imasleval  13405  lsmspsn  15799  metrest  18032  nmoo0  21329  hhcmpl  21739  nmop0  22526  nmfn0  22527  axfelem18  23732  axsegcon  23930  axeuclid  23966  prtlem11  26101  prter2  26116  prter3  26117  diophrex  26222  islshpat  28374  lshpsmreu  28466  islpln5  28891  islvol5  28935  cdlemftr3  29921  dvhb1dimN  30342  dib1dim  30522  mapdpglem3  31032  hdmapglem7a  31287
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 2524
  Copyright terms: Public domain W3C validator