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

Theorem r19.21bi 2768
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 2765 . . 3  |-  ( A. x  e.  A  ps  ->  ( x  e.  A  ->  ps ) )
31, 2syl 17 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
43imp 435 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1897   A.wral 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-12 1943
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-ral 2753
This theorem is referenced by:  r19.21be  2770  rspec2  2771  rspec3  2772  ralxfr2d  4629  f1oresrab  6078  isoselem  6256  boxcutc  7590  xpf1o  7759  fineqvlem  7811  indexfi  7907  dffi3  7970  suppr  8012  supiso  8016  infpr  8044  ordtypelem9  8066  brwdom3  8122  xpwdomg  8125  ixpiunwdom  8131  infxpenc2lem1  8475  hsmexlem4  8884  gchina  9149  wunom  9170  prcdnq  9443  prnmax  9445  dedekind  9822  dedekindle  9823  monoord2  12275  seqshft  13196  limsupgre  13590  limsupgreOLD  13591  limsupbnd1  13592  limsupbnd1OLD  13593  limsupbnd2  13594  limsupbnd2OLD  13595  climmpt2  13685  rlimcld2  13690  rlimmptrcl  13719  lo1mptrcl  13733  o1mptrcl  13734  climsup  13781  sumpr  13857  sumtp  13858  fsum2dlem  13879  fsumiun  13929  fprod2dlem  14082  iserodd  14833  vdwlem1  14979  vdwlem6  14984  vdwnnlem3  14995  imasvscafn  15491  fuciso  15928  evlfcl  16155  yonedainv  16214  acsmapd  16472  prdsmndd  16617  psgnunilem5  17183  gsummpt1n0  17645  dprdspan  17708  ablfaclem2  17767  srgi  17793  srgrz  17807  srglz  17808  issrngd  18137  psrbaglesupp  18640  psrbagcon  18643  psrass1lem  18649  evlslem2  18783  mpfind  18807  gsumsmonply1  18945  gsummoncoe1  18946  evl1gsummon  19001  frgpcyg  19192  frlmgsum  19378  uvcresum  19399  cpmatmcllem  19790  neiptoptop  20195  neiptopnei  20196  ordtrest2lem  20267  cncmp  20455  1stckgenlem  20616  ptcld  20676  dfac14  20681  txcnp  20683  ptcnplem  20684  ptcnp  20685  ptcn  20690  pthaus  20701  xkococnlem  20722  xkococn  20723  cnmpt11  20726  cnmpt1t  20728  cnmpt12  20730  cnmptkp  20743  cnmptk1  20744  cnmptkk  20746  cnmptk1p  20748  cnmptk2  20749  cnmpt2k  20751  xpstopnlem1  20872  cnpflfi  21062  ptcmplem2  21116  cnextcn  21130  cnextfres1  21131  cnmpt1plusg  21150  cnmpt2plusg  21151  cnmpt1vsca  21256  cnmpt2vsca  21257  ustfilxp  21275  utoptop  21297  restutop  21300  restutopopn  21301  ucncn  21348  cfilufg  21356  trcfilu  21357  psmet0  21372  psmettri2  21373  prdsxmetlem  21431  prdsbl  21554  prdsxmslem2  21592  psmetutop  21630  cnmpt1ds  21908  cnmpt2ds  21909  cncfmpt2ss  21995  bndth  22034  cnmpt1ip  22266  cnmpt2ip  22267  iscmet3lem2  22310  cmetcusp1  22368  rrxcph  22399  ovoliunlem1  22503  ovoliunlem3  22505  ovoliun  22506  ovoliun2  22507  ovolscalem1  22514  volfiniun  22548  uniioombllem4  22592  mbfmptcl  22641  mbfeqalem  22646  mbfres2  22649  ismbf3d  22658  mbfsup  22668  mbfinf  22669  mbfinfOLD  22670  mbflim  22674  itg1ge0  22692  itg1mulc  22710  i1fposd  22713  itg1climres  22720  mbfi1fseqlem4  22724  itg2lea  22750  itg2splitlem  22754  itg2split  22755  itg2monolem1  22756  itg2mono  22759  itg2i1fseqle  22760  itg2i1fseq  22761  itg2addlem  22764  itg2cnlem1  22767  itgeqa  22819  itgss3  22820  itgfsum  22832  itgabs  22840  itggt0  22847  dvmptcl  22961  dvmptco  22974  dvlipcn  22994  dvle  23007  dvfsumle  23021  dvfsumge  23022  dvfsumabs  23023  dvmptrecl  23024  dvfsumlem2  23027  itgparts  23047  itgsubstlem  23048  itgsubst  23049  coeeulem  23226  dgrlem  23231  dgrlb  23238  coeaddlem  23251  coecj  23280  ulmss  23400  ulmdvlem2  23404  itgulm2  23412  logtayl  23653  leibpi  23916  xrlimcnp  23942  o1cxp  23948  jensen  23962  lgambdd  24010  wilthlem2  24042  sqff1o  24157  fsumdvdscom  24162  fsumdvdsmul  24172  dchrmulcl  24225  dchrmulid2  24228  dchrinv  24237  dchrisumlem3  24377  dchrvmasumlem2  24384  ostth1  24519  ercgrg  24610  f1otrg  24949  f1otrge  24950  ubthlem2  26561  fmptcof2  28307  disjdsct  28331  ressprs  28464  oduprs  28465  archiabl  28563  lmodslmd  28568  txomap  28709  qtophaus  28711  locfinreflem  28715  ordtrest2NEWlem  28776  lmdvg  28807  esumcl  28899  esumeq2d  28906  esumnul  28917  hasheuni  28954  esumcvg  28955  esumcvgre  28960  insiga  29007  ldsysgenld  29030  ldgenpisyslem1  29033  measvunilem  29082  measvunilem0  29083  measdivcstOLD  29094  cntmeas  29096  voliune  29100  volfiniune  29101  1stmbfm  29130  2ndmbfm  29131  omssubadd  29176  omssubaddOLD  29180  difelcarsg  29190  inelcarsg  29191  eulerpartlems  29241  eulerpartlemsv3  29242  eulerpartlemgvv  29257  dstrvprob  29352  bnj93  29722  bnj518  29745  bnj1489  29913  subfacp1lem3  29953  subfacp1lem5  29955  erdszelem8  29969  ptpcon  30004  rescon  30017  cvmliftmolem2  30053  cvmlift2lem11  30084  cvmliftphtlem  30088  mclsax  30255  fin2so  31976  poimirlem18  32002  poimirlem21  32005  mblfinlem2  32022  itgabsnc  32055  itggt0cn  32058  prdsbnd  32169  prdstotbnd  32170  prdsbnd2  32171  rrnequiv  32211  eqlkr3  32711  dih1dimatlem  34941  fnwe2lem1  35952  imo72b2  36662  rfcnnnub  37396  disjxp1  37448  mptex2  37470  fompt  37504  suplesup  37599  climinf  37721  climinfOLD  37722  climsuse  37724  mullimc  37733  limccog  37737  mullimcf  37740  limcperiod  37745  limcleqr  37762  neglimc  37765  0ellimcdiv  37767  limclner  37769  dvdivbd  37832  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem1OLD  37842  dvnprodlem2  37859  iblsplit  37880  stoweidlem5  37902  stoweidlem16  37913  stoweidlem21  37918  stoweidlem24  37921  stoweidlem25  37922  stoweidlem28  37925  stoweidlem31  37929  stoweidlem41  37939  stoweidlem42  37940  stoweidlem44  37942  stoweidlem45  37943  stoweidlem48  37946  stoweidlem51  37949  stoweidlem54  37952  stoweidlem57  37955  stoweidlem60  37958  stoweidlem62  37960  stoweidlem62OLD  37961  stirlinglem5  37977  dirkercncflem3  38004  fourierdlem11  38017  fourierdlem12  38018  fourierdlem14  38020  fourierdlem15  38021  fourierdlem31  38037  fourierdlem31OLD  38038  fourierdlem34  38041  fourierdlem41  38048  fourierdlem48  38055  fourierdlem49  38056  fourierdlem50  38057  fourierdlem54  38061  fourierdlem69  38076  fourierdlem73  38080  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem79  38086  fourierdlem80  38087  fourierdlem81  38088  fourierdlem92  38099  fourierdlem93  38100  fourierdlem94  38101  fourierdlem97  38104  fourierdlem103  38110  fourierdlem104  38111  fourierdlem111  38118  fourierdlem113  38120  etransclem32  38168  sge0rpcpnf  38300  caragendifcl  38372
  Copyright terms: Public domain W3C validator