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

Theorem r19.21bi 2764
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 2671 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 189 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1770 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 419 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546    e. wcel 1721   A.wral 2666
This theorem is referenced by:  rspec2  2765  rspec3  2766  r19.21be  2767  reusv6OLD  4693  ralxfr2d  4698  isoselem  6020  boxcutc  7064  xpf1o  7228  fineqvlem  7282  indexfi  7372  dffi3  7394  suppr  7429  supiso  7433  ordtypelem9  7451  brwdom3  7506  xpwdomg  7509  ixpiunwdom  7515  infxpenc2lem1  7856  hsmexlem4  8265  gchina  8530  wunom  8551  prcdnq  8826  prnmax  8828  monoord2  11309  seqshft  11855  limsupgre  12230  limsupbnd1  12231  limsupbnd2  12232  climmpt2  12322  rlimcld2  12327  rlimmptrcl  12356  lo1mptrcl  12370  o1mptrcl  12371  climsup  12418  fsum2dlem  12509  fsumiun  12555  iserodd  13164  vdwlem1  13304  vdwlem6  13309  vdwnnlem3  13320  imasvscafn  13717  fuciso  14127  evlfcl  14274  yonedainv  14333  acsmapd  14559  prdsmndd  14683  dprdspan  15540  ablfaclem2  15599  issrngd  15904  psrbaglesupp  16388  psrbagcon  16391  psrass1lem  16397  evlslem2  16523  frgpcyg  16809  neiptoptop  17150  neiptopnei  17151  ordtrest2lem  17221  cncmp  17409  1stckgenlem  17538  ptcld  17598  dfac14  17603  txcnp  17605  ptcnplem  17606  ptcnp  17607  ptcn  17612  pthaus  17623  xkococnlem  17644  xkococn  17645  cnmpt11  17648  cnmpt1t  17650  cnmpt12  17652  cnmptkp  17665  cnmptk1  17666  cnmptkk  17668  cnmptk1p  17670  cnmptk2  17671  cnmpt2k  17673  xpstopnlem1  17794  cnpflfi  17984  ptcmplem2  18037  cnextcn  18051  cnextfres  18052  cnmpt1plusg  18070  cnmpt2plusg  18071  cnmpt1vsca  18176  cnmpt2vsca  18177  ustfilxp  18195  utoptop  18217  restutop  18220  restutopopn  18221  ucncn  18268  cfilufg  18276  trcfilu  18277  psmet0  18292  psmettri2  18293  prdsxmetlem  18351  prdsbl  18474  prdsxmslem2  18512  metutopOLD  18565  psmetutop  18566  cnmpt1ds  18826  cnmpt2ds  18827  cncfmpt2ss  18898  bndth  18936  cnmpt1ip  19154  cnmpt2ip  19155  iscmet3lem2  19198  cmetcusp1OLD  19258  cmetcusp1  19259  ovoliunlem1  19351  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  ovolscalem1  19362  volfiniun  19394  uniioombllem4  19431  mbfmptcl  19482  mbfeqalem  19487  mbfres2  19490  ismbf3d  19499  mbfsup  19509  mbfinf  19510  mbflim  19513  itg1ge0  19531  itg1mulc  19549  i1fposd  19552  itg1climres  19559  mbfi1fseqlem4  19563  itg2lea  19589  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2addlem  19603  itg2cnlem1  19606  itgeqa  19658  itgss3  19659  itgfsum  19671  itgabs  19679  itggt0  19686  dvmptcl  19798  dvmptco  19811  dvlipcn  19831  dvle  19844  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvmptrecl  19861  dvfsumlem2  19864  itgparts  19884  itgsubstlem  19885  itgsubst  19886  mpfind  19918  coeeulem  20096  dgrlem  20101  dgrlb  20108  coeaddlem  20120  coecj  20149  ulmss  20266  ulmdvlem2  20270  itgulm2  20278  logtayl  20504  leibpi  20735  xrlimcnp  20760  o1cxp  20766  jensen  20780  wilthlem2  20805  sqff1o  20918  fsumdvdscom  20923  fsumdvdsmul  20933  dchrmulcl  20986  dchrmulid2  20989  dchrinv  20998  dchrisumlem3  21138  dchrvmasumlem2  21145  ostth1  21280  ubthlem2  22326  abrexss  23946  ofrn  24005  fmptcof2  24029  disjdsct  24043  sumpr  24171  kerf1hrm  24215  lmdvg  24291  esumcl  24380  esumeq2d  24387  esumnul  24396  hasheuni  24428  esumcvg  24429  insiga  24473  measvunilem  24519  measvunilem0  24520  measdivcstOLD  24531  cntmeas  24533  voliune  24538  volfiniune  24539  1stmbfm  24563  2ndmbfm  24564  sitgf  24613  dstrvprob  24682  lgambdd  24774  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem8  24837  ptpcon  24873  rescon  24886  cvmliftmolem2  24922  cvmlift2lem11  24953  cvmliftphtlem  24957  dedekind  25140  dedekindle  25141  fprod2dlem  25257  mblfinlem  26143  itgabsnc  26173  itggt0cn  26176  prdsbnd  26392  prdstotbnd  26393  prdsbnd2  26394  rrnequiv  26434  fnwe2lem1  27015  frlmgsum  27100  uvcresum  27110  psgnunilem5  27285  rfcnnnub  27574  climinf  27599  climsuse  27601  stoweidlem5  27621  stoweidlem16  27632  stoweidlem21  27637  stoweidlem24  27640  stoweidlem25  27641  stoweidlem28  27644  stoweidlem31  27647  stoweidlem41  27657  stoweidlem42  27658  stoweidlem44  27660  stoweidlem45  27661  stoweidlem48  27664  stoweidlem51  27667  stoweidlem54  27670  stoweidlem57  27673  stoweidlem60  27676  stoweidlem62  27678  stirlinglem5  27694  bnj93  28940  bnj518  28963  bnj1489  29131  eqlkr3  29584  dih1dimatlem  31812
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2671
  Copyright terms: Public domain W3C validator