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

Theorem r19.21bi 2643
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
r19.21bi.1  |-  ( ph  ->  A. x  e.  A  ps )
Assertion
Ref Expression
r19.21bi  |-  ( (
ph  /\  x  e.  A )  ->  ps )

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . . 4  |-  ( ph  ->  A. x  e.  A  ps )
2 df-ral 2550 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 188 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1796 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 418 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1529    e. wcel 1686   A.wral 2545
This theorem is referenced by:  rspec2  2644  rspec3  2645  r19.21be  2646  reusv6OLD  4547  ralxfr2d  4552  isoselem  5840  boxcutc  6861  xpf1o  7025  fineqvlem  7079  indexfi  7165  dffi3  7186  suppr  7221  supiso  7225  ordtypelem9  7243  brwdom3  7298  xpwdomg  7301  ixpiunwdom  7307  infxpenc2lem1  7648  hsmexlem4  8057  gchina  8323  wunom  8344  prcdnq  8619  prnmax  8621  monoord2  11079  seqshft  11582  limsupgre  11957  limsupbnd1  11958  limsupbnd2  11959  climmpt2  12049  rlimcld2  12054  rlimmptrcl  12083  lo1mptrcl  12097  o1mptrcl  12098  climsup  12145  fsum2dlem  12235  fsumiun  12281  iserodd  12890  vdwlem1  13030  vdwlem6  13035  vdwnnlem3  13046  imasvscafn  13441  fuciso  13851  evlfcl  13998  yonedalem3b  14055  yonedainv  14057  acsmapd  14283  prdsmndd  14407  dprdspan  15264  ablfaclem2  15323  issrngd  15628  psrbaglesupp  16116  psrbagcon  16119  psrass1lem  16125  evlslem2  16251  frgpcyg  16529  ordtrest2lem  16935  cncmp  17121  1stckgenlem  17250  ptcld  17309  dfac14  17314  txcnp  17316  ptcnplem  17317  ptcnp  17318  ptcn  17323  pthaus  17334  xkococnlem  17355  xkococn  17356  cnmpt11  17359  cnmpt1t  17361  cnmpt12  17363  cnmptkp  17376  cnmptk1  17377  cnmptkk  17379  cnmptk1p  17381  cnmptk2  17382  cnmpt2k  17384  xpstopnlem1  17502  cnpflfi  17696  ptcmplem2  17749  cnmpt1plusg  17772  cnmpt2plusg  17773  cnmpt1vsca  17878  cnmpt2vsca  17879  prdsxmetlem  17934  prdsbl  18039  prdsxmslem2  18077  cnmpt1ds  18349  cnmpt2ds  18350  cncfmpt2ss  18421  bndth  18458  cnmpt1ip  18676  cnmpt2ip  18677  iscmet3lem2  18720  ovoliunlem1  18863  ovoliunlem3  18865  ovoliun  18866  ovoliun2  18867  ovolscalem1  18874  volfiniun  18906  uniioombllem4  18943  mbfmptcl  18994  mbfeqalem  18999  mbfres2  19002  ismbf3d  19011  mbfsup  19021  mbfinf  19022  mbflim  19025  itg1ge0  19043  itg1mulc  19061  i1fposd  19064  itg1climres  19071  mbfi1fseqlem4  19075  itg2lea  19101  itg2splitlem  19105  itg2split  19106  itg2monolem1  19107  itg2mono  19110  itg2i1fseqle  19111  itg2i1fseq  19112  itg2addlem  19115  itg2cnlem1  19118  itgeqa  19170  itgss3  19171  itgfsum  19183  itgabs  19191  itggt0  19198  dvmptcl  19310  dvmptco  19323  dvlipcn  19343  dvle  19356  dvfsumle  19370  dvfsumge  19371  dvfsumabs  19372  dvmptrecl  19373  dvfsumlem2  19376  itgparts  19396  itgsubstlem  19397  itgsubst  19398  mpfind  19430  coeeulem  19608  dgrlem  19613  dgrlb  19620  coeaddlem  19632  coecj  19661  ulmss  19776  ulmdvlem2  19780  itgulm2  19787  logtayl  20009  leibpi  20240  xrlimcnp  20265  o1cxp  20271  jensen  20285  wilthlem2  20309  sqff1o  20422  fsumdvdscom  20427  fsumdvdsmul  20437  dchrmulcl  20490  dchrmulid2  20493  dchrinv  20502  dchrisumlem3  20642  dchrvmasumlem2  20649  ostth1  20784  ubthlem2  21452  abrexss  23042  sumpr  23170  ofrn  23208  fmptcof2  23231  disjdsct  23371  lmdvg  23378  esumcl  23415  esumeq2d  23421  esumnul  23429  hasheuni  23455  esumcvg  23456  ofcfval4  23468  insiga  23500  measvunilem  23542  measvunilem0  23543  measdivcstOLD  23553  measdivcst  23554  cntmeas  23555  1stmbfm  23567  2ndmbfm  23568  imambfm  23569  itgmeq123dTMP  23591  dstrvprob  23674  subfacp1lem3  23715  subfacp1lem5  23717  erdszelem8  23731  ptpcon  23766  rescon  23779  cvmliftmolem2  23815  cvmlift2lem11  23846  cvmliftphtlem  23850  dedekind  24084  dedekindle  24085  supwlub  25285  prdsbnd  26528  prdstotbnd  26529  prdsbnd2  26530  rrnequiv  26570  fnwe2lem1  27158  frlmgsum  27243  uvcresum  27253  psgnunilem5  27428  climinf  27743  climsuse  27745  stoweidlem16  27776  stoweidlem21  27781  stoweidlem24  27784  stoweidlem31  27791  stoweidlem41  27801  stoweidlem42  27802  stoweidlem51  27811  stoweidlem57  27817  stoweidlem60  27820  stirlinglem5  27838  bnj93  28968  bnj518  28991  bnj1489  29159  eqlkr3  29364  dih1dimatlem  31592
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2550
  Copyright terms: Public domain W3C validator