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

Theorem r19.41v 2853
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 2852 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wrex 2698
This theorem is referenced by:  r19.42v  2854  3reeanv  2868  reuind  3129  iuncom4  4092  dfiun2g  4115  iunxiun  4165  inuni  4354  reuxfrd  4739  xpiundi  4923  xpiundir  4924  imaco  5366  coiun  5370  abrexco  5977  imaiun  5983  isomin  6048  isoini  6049  oarec  6796  mapsnen  7175  genpass  8875  4fvwrd4  11109  4sqlem12  13312  imasleval  13754  lsmspsn  16144  utoptop  18252  metrest  18542  metustOLD  18585  metust  18586  cfilucfilOLD  18587  cfilucfil  18588  metuel2  18597  nmoo0  22280  hhcmpl  22690  nmop0  23477  nmfn0  23478  r19.41vv  23958  reuxfr4d  23965  rexunirn  23966  dya2icoseg2  24616  dya2iocnei  24620  nofulllem5  25615  elfuns  25710  axsegcon  25814  axeuclid  25850  rabiun2  26186  ismblfin  26193  itg2addnclem3  26204  prtlem11  26652  prter2  26667  prter3  26668  diophrex  26771  usgreg2spot  28314  islshpat  29654  lshpsmreu  29746  islpln5  30171  islvol5  30215  cdlemftr3  31201  dvhb1dimN  31622  dib1dim  31802  mapdpglem3  32312  hdmapglem7a  32567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-rex 2703
  Copyright terms: Public domain W3C validator