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

Theorem r19.21bi 2833
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.)
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 . . 3  |-  ( ph  ->  A. x  e.  A  ps )
2 rsp 2830 . . 3  |-  ( A. x  e.  A  ps  ->  ( x  e.  A  ->  ps ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
43imp 429 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819
This theorem is referenced by:  r19.21be  2835  rspec2  2836  rspec3  2837  reusv6OLD  4658  ralxfr2d  4663  f1oresrab  6051  isoselem  6223  boxcutc  7509  xpf1o  7676  fineqvlem  7731  indexfi  7824  dffi3  7887  suppr  7925  supiso  7929  ordtypelem9  7947  brwdom3  8004  xpwdomg  8007  ixpiunwdom  8013  infxpenc2lem1  8392  hsmexlem4  8805  gchina  9073  wunom  9094  prcdnq  9367  prnmax  9369  dedekind  9739  dedekindle  9740  monoord2  12101  seqshft  12875  limsupgre  13260  limsupbnd1  13261  limsupbnd2  13262  climmpt2  13352  rlimcld2  13357  rlimmptrcl  13386  lo1mptrcl  13400  o1mptrcl  13401  climsup  13448  fsum2dlem  13541  fsumiun  13591  iserodd  14211  vdwlem1  14351  vdwlem6  14356  vdwnnlem3  14367  imasvscafn  14785  fuciso  15195  evlfcl  15342  yonedainv  15401  acsmapd  15658  prdsmndd  15764  psgnunilem5  16312  gsummpt1n0  16780  dprdspan  16861  ablfaclem2  16924  srgi  16950  srgrz  16964  srglz  16965  issrngd  17290  psrbaglesupp  17785  psrbaglesuppOLD  17786  psrbagcon  17790  psrass1lem  17797  evlslem2  17948  mpfind  17973  gsumsmonply1  18113  gsummoncoe1  18114  evl1gsummon  18169  frgpcyg  18376  frlmgsumOLD  18565  frlmgsum  18566  uvcresum  18588  cpmatmcllem  18983  neiptoptop  19395  neiptopnei  19396  ordtrest2lem  19467  cncmp  19655  1stckgenlem  19786  ptcld  19846  dfac14  19851  txcnp  19853  ptcnplem  19854  ptcnp  19855  ptcn  19860  pthaus  19871  xkococnlem  19892  xkococn  19893  cnmpt11  19896  cnmpt1t  19898  cnmpt12  19900  cnmptkp  19913  cnmptk1  19914  cnmptkk  19916  cnmptk1p  19918  cnmptk2  19919  cnmpt2k  19921  xpstopnlem1  20042  cnpflfi  20232  ptcmplem2  20285  cnextcn  20299  cnextfres  20300  cnmpt1plusg  20318  cnmpt2plusg  20319  cnmpt1vsca  20428  cnmpt2vsca  20429  ustfilxp  20447  utoptop  20469  restutop  20472  restutopopn  20473  ucncn  20520  cfilufg  20528  trcfilu  20529  psmet0  20544  psmettri2  20545  prdsxmetlem  20603  prdsbl  20726  prdsxmslem2  20764  metutopOLD  20817  psmetutop  20818  cnmpt1ds  21079  cnmpt2ds  21080  cncfmpt2ss  21151  bndth  21190  cnmpt1ip  21419  cnmpt2ip  21420  iscmet3lem2  21463  cmetcusp1OLD  21523  cmetcusp1  21524  rrxcph  21556  ovoliunlem1  21645  ovoliunlem3  21647  ovoliun  21648  ovoliun2  21649  ovolscalem1  21656  volfiniun  21689  uniioombllem4  21727  mbfmptcl  21776  mbfeqalem  21781  mbfres2  21784  ismbf3d  21793  mbfsup  21803  mbfinf  21804  mbflim  21807  itg1ge0  21825  itg1mulc  21843  i1fposd  21846  itg1climres  21853  mbfi1fseqlem4  21857  itg2lea  21883  itg2splitlem  21887  itg2split  21888  itg2monolem1  21889  itg2mono  21892  itg2i1fseqle  21893  itg2i1fseq  21894  itg2addlem  21897  itg2cnlem1  21900  itgeqa  21952  itgss3  21953  itgfsum  21965  itgabs  21973  itggt0  21980  dvmptcl  22094  dvmptco  22107  dvlipcn  22127  dvle  22140  dvfsumle  22154  dvfsumge  22155  dvfsumabs  22156  dvmptrecl  22157  dvfsumlem2  22160  itgparts  22180  itgsubstlem  22181  itgsubst  22182  coeeulem  22353  dgrlem  22358  dgrlb  22365  coeaddlem  22377  coecj  22406  ulmss  22523  ulmdvlem2  22527  itgulm2  22535  logtayl  22766  leibpi  22998  xrlimcnp  23023  o1cxp  23029  jensen  23043  wilthlem2  23068  sqff1o  23181  fsumdvdscom  23186  fsumdvdsmul  23196  dchrmulcl  23249  dchrmulid2  23252  dchrinv  23261  dchrisumlem3  23401  dchrvmasumlem2  23408  ostth1  23543  tgtrisegint  23615  ercgrg  23633  f1otrg  23847  f1otrge  23848  elntg  23960  ubthlem2  25460  abrexss  27081  ofrn  27149  fmptcof2  27171  fcnvgreu  27183  disjdsct  27190  ressprs  27302  oduprs  27303  submarchi  27389  archiabl  27401  lmodslmd  27406  sumpr  27428  txomap  27497  ordtrest2NEWlem  27537  lmdvg  27568  qtophaus  27634  esumcl  27680  esumeq2d  27687  esumnul  27696  hasheuni  27728  esumcvg  27729  insiga  27774  measvunilem  27820  measvunilem0  27821  measdivcstOLD  27832  cntmeas  27834  voliune  27838  volfiniune  27839  1stmbfm  27868  2ndmbfm  27869  sitgf  27926  eulerpartlems  27936  eulerpartlemsv3  27937  eulerpartgbij  27948  eulerpartlemgvv  27952  sseqf  27968  dstrvprob  28047  signsvvfval  28172  lgambdd  28216  subfacp1lem3  28263  subfacp1lem5  28265  erdszelem8  28279  ptpcon  28315  rescon  28328  cvmliftmolem2  28364  cvmlift2lem11  28395  cvmliftphtlem  28399  fprod2dlem  28684  fin2so  29614  mblfinlem2  29627  itgabsnc  29659  itggt0cn  29662  prdsbnd  29890  prdstotbnd  29891  prdsbnd2  29892  rrnequiv  29932  fnwe2lem1  30600  rfcnnnub  30989  mptex2  31023  climinf  31148  climsuse  31150  mullimc  31158  limccog  31162  mullimcf  31165  limcperiod  31170  limcleqr  31186  neglimc  31189  0ellimcdiv  31191  limclner  31193  dvdivbd  31253  ioodvbdlimc1lem1  31261  stoweidlem5  31305  stoweidlem16  31316  stoweidlem21  31321  stoweidlem24  31324  stoweidlem25  31325  stoweidlem28  31328  stoweidlem31  31331  stoweidlem41  31341  stoweidlem42  31342  stoweidlem44  31344  stoweidlem45  31345  stoweidlem48  31348  stoweidlem51  31351  stoweidlem54  31354  stoweidlem57  31357  stoweidlem60  31360  stoweidlem62  31362  stirlinglem5  31378  dirkercncflem3  31405  fourierdlem11  31418  fourierdlem12  31419  fourierdlem14  31421  fourierdlem15  31422  fourierdlem31  31438  fourierdlem34  31441  fourierdlem41  31448  fourierdlem45  31452  fourierdlem50  31457  fourierdlem54  31461  fourierdlem69  31476  fourierdlem74  31481  fourierdlem75  31482  fourierdlem79  31486  fourierdlem81  31488  fourierdlem92  31499  fourierdlem93  31500  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem113  31520  bnj93  33000  bnj518  33023  bnj1489  33191  eqlkr3  33898  dih1dimatlem  36126
  Copyright terms: Public domain W3C validator