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

Theorem r19.41v 2994
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 1692 . 2  |-  F/ x ps
21r19.41 2993 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 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-nf 1602  df-rex 2797
This theorem is referenced by:  r19.41vv  2995  r19.42v  2996  3reeanv  3010  reuind  3287  iuncom4  4320  dfiun2g  4344  iunxiun  4395  inuni  4596  reuxfrd  4659  xpiundi  5041  xpiundir  5042  imaco  5499  coiun  5504  abrexco  6138  imaiun  6139  isomin  6215  isoini  6216  oarec  7210  mapsnen  7592  genpass  9387  4fvwrd4  11798  4sqlem12  14348  imasleval  14812  lsmspsn  17601  utoptop  20607  metrest  20897  metustOLD  20940  metust  20941  cfilucfilOLD  20942  cfilucfil  20943  metuel2  20952  istrkg2ld  23727  axsegcon  24099  usgreg2spot  24936  nmoo0  25575  hhcmpl  25986  nmop0  26774  nmfn0  26775  reuxfr4d  27258  rexunirn  27259  ordtconlem1  27776  dya2icoseg2  28119  dya2iocnei  28123  nofulllem5  29438  rabiun  30008  iundif1  30009  ismblfin  30027  prtlem11  30579  prter2  30594  prter3  30595  diophrex  30681  islshpat  34465  lshpsmreu  34557  islpln5  34982  islvol5  35026  cdlemftr3  36014  dvhb1dimN  36435  dib1dim  36615  mapdpglem3  37125  hdmapglem7a  37380
  Copyright terms: Public domain W3C validator