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

Theorem r19.41v 2871
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 1673 . 2  |-  F/ x ps
21r19.41 2870 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wrex 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-rex 2719
This theorem is referenced by:  r19.41vv  2872  r19.42v  2873  3reeanv  2887  reuind  3160  iuncom4  4176  dfiun2g  4200  iunxiun  4251  inuni  4452  reuxfrd  4515  xpiundi  4891  xpiundir  4892  imaco  5341  coiun  5345  abrexco  5959  imaiun  5960  isomin  6026  isoini  6027  oarec  6999  mapsnen  7385  genpass  9176  4fvwrd4  11531  4sqlem12  14015  imasleval  14477  lsmspsn  17163  utoptop  19807  metrest  20097  metustOLD  20140  metust  20141  cfilucfilOLD  20142  cfilucfil  20143  metuel2  20152  axsegcon  23171  axeuclid  23207  nmoo0  24189  hhcmpl  24600  nmop0  25388  nmfn0  25389  reuxfr4d  25872  rexunirn  25873  ordtconlem1  26352  dya2icoseg2  26691  dya2iocnei  26695  nofulllem5  27845  rabiun  28409  iundif1  28410  ismblfin  28429  itg2addnclem3  28442  prtlem11  29008  prter2  29023  prter3  29024  diophrex  29111  usgreg2spot  30657  islshpat  32659  lshpsmreu  32751  islpln5  33176  islvol5  33220  cdlemftr3  34206  dvhb1dimN  34627  dib1dim  34807  mapdpglem3  35317  hdmapglem7a  35572
  Copyright terms: Public domain W3C validator