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

Theorem r19.29 2963
Description: Restricted quantifier version of 19.29 1728. See also r19.29r 2964. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.29  |-  ( ( A. x  e.  A  ph 
/\  E. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )

Proof of Theorem r19.29
StepHypRef Expression
1 pm3.2 448 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2818 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2890 . . 3  |-  ( A. x  e.  A  ( ps  ->  ( ph  /\  ps ) )  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
42, 3syl 17 . 2  |-  ( A. x  e.  A  ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
54imp 430 1  |-  ( ( A. x  e.  A  ph 
/\  E. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   A.wral 2775   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781
This theorem is referenced by:  r19.29r  2964  r19.29d2r  2971  disjiun  4411  triun  4528  ralxfrd  4631  elrnmptg  5099  fmpt  6054  fliftfun  6216  fun11iun  6763  omabs  7352  findcard3  7816  r1sdom  8246  tcrank  8356  infxpenlem  8445  dfac12k  8577  cfslb2n  8698  cfcoflem  8702  iundom2g  8965  supsrlem  9535  axpre-sup  9593  fimaxre3  10553  limsupbnd2  13531  limsupbnd2OLD  13532  rlimuni  13599  rlimcld2  13627  rlimno1  13702  pgpfac1lem5  17697  ppttop  20006  epttop  20008  tgcnp  20253  lmcnp  20304  bwth  20409  1stcrest  20452  txlm  20647  tx1stc  20649  fbfinnfr  20840  fbunfip  20868  filuni  20884  ufileu  20918  fbflim2  20976  flftg  20995  ufilcmp  21031  cnpfcf  21040  tsmsxp  21153  metss  21507  lmmbr  22212  ivthlem2  22387  ivthlem3  22388  dyadmax  22540  rhmdvdsr  28574  tpr2rico  28711  esumpcvgval  28892  sigaclcuni  28933  voliune  29045  volfiniune  29046  dya2icoseg2  29093  poimirlem29  31880  unirep  31950  heibor1lem  32052  2r19.29  32341  pmapglbx  33250  stoweidlem35  37713  ralxfrd2  38706
  Copyright terms: Public domain W3C validator