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

Theorem r19.41v 3014
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 1683 . 2  |-  F/ x ps
21r19.41 3013 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 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-rex 2820
This theorem is referenced by:  r19.41vv  3015  r19.42v  3016  3reeanv  3030  reuind  3307  iuncom4  4333  dfiun2g  4357  iunxiun  4408  inuni  4609  reuxfrd  4672  xpiundi  5054  xpiundir  5055  imaco  5512  coiun  5517  abrexco  6144  imaiun  6145  isomin  6221  isoini  6222  oarec  7211  mapsnen  7593  genpass  9387  4fvwrd4  11790  4sqlem12  14333  imasleval  14796  lsmspsn  17530  utoptop  20500  metrest  20790  metustOLD  20833  metust  20834  cfilucfilOLD  20835  cfilucfil  20836  metuel2  20845  istrkg2ld  23614  axsegcon  23934  axeuclid  23970  usgreg2spot  24772  nmoo0  25410  hhcmpl  25821  nmop0  26609  nmfn0  26610  reuxfr4d  27093  rexunirn  27094  ordtconlem1  27570  dya2icoseg2  27917  dya2iocnei  27921  nofulllem5  29071  rabiun  29641  iundif1  29642  ismblfin  29660  itg2addnclem3  29673  prtlem11  30239  prter2  30254  prter3  30255  diophrex  30341  islshpat  33832  lshpsmreu  33924  islpln5  34349  islvol5  34393  cdlemftr3  35379  dvhb1dimN  35800  dib1dim  35980  mapdpglem3  36490  hdmapglem7a  36745
  Copyright terms: Public domain W3C validator