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

Theorem r19.21bi 2920
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 2804 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 196 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1809 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 429 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1368    e. wcel 1758   A.wral 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-ral 2804
This theorem is referenced by:  rspec2  2921  rspec3  2922  r19.21be  2923  reusv6OLD  4612  ralxfr2d  4617  f1oresrab  5985  isoselem  6142  boxcutc  7417  xpf1o  7584  fineqvlem  7639  indexfi  7731  dffi3  7793  suppr  7830  supiso  7834  ordtypelem9  7852  brwdom3  7909  xpwdomg  7912  ixpiunwdom  7918  infxpenc2lem1  8297  hsmexlem4  8710  gchina  8978  wunom  8999  prcdnq  9274  prnmax  9276  dedekind  9645  dedekindle  9646  monoord2  11955  seqshft  12693  limsupgre  13078  limsupbnd1  13079  limsupbnd2  13080  climmpt2  13170  rlimcld2  13175  rlimmptrcl  13204  lo1mptrcl  13218  o1mptrcl  13219  climsup  13266  fsum2dlem  13356  fsumiun  13403  iserodd  14021  vdwlem1  14161  vdwlem6  14166  vdwnnlem3  14177  imasvscafn  14595  fuciso  15005  evlfcl  15152  yonedainv  15211  acsmapd  15468  prdsmndd  15574  psgnunilem5  16120  gsummpt1n0  16579  dprdspan  16647  ablfaclem2  16710  srgi  16736  srgrz  16750  srglz  16751  issrngd  17070  psrbaglesupp  17559  psrbaglesuppOLD  17560  psrbagcon  17564  psrass1lem  17571  evlslem2  17722  mpfind  17747  evl1gsummon  17925  frgpcyg  18132  frlmgsumOLD  18321  frlmgsum  18322  uvcresum  18344  neiptoptop  18868  neiptopnei  18869  ordtrest2lem  18940  cncmp  19128  1stckgenlem  19259  ptcld  19319  dfac14  19324  txcnp  19326  ptcnplem  19327  ptcnp  19328  ptcn  19333  pthaus  19344  xkococnlem  19365  xkococn  19366  cnmpt11  19369  cnmpt1t  19371  cnmpt12  19373  cnmptkp  19386  cnmptk1  19387  cnmptkk  19389  cnmptk1p  19391  cnmptk2  19392  cnmpt2k  19394  xpstopnlem1  19515  cnpflfi  19705  ptcmplem2  19758  cnextcn  19772  cnextfres  19773  cnmpt1plusg  19791  cnmpt2plusg  19792  cnmpt1vsca  19901  cnmpt2vsca  19902  ustfilxp  19920  utoptop  19942  restutop  19945  restutopopn  19946  ucncn  19993  cfilufg  20001  trcfilu  20002  psmet0  20017  psmettri2  20018  prdsxmetlem  20076  prdsbl  20199  prdsxmslem2  20237  metutopOLD  20290  psmetutop  20291  cnmpt1ds  20552  cnmpt2ds  20553  cncfmpt2ss  20624  bndth  20663  cnmpt1ip  20892  cnmpt2ip  20893  iscmet3lem2  20936  cmetcusp1OLD  20996  cmetcusp1  20997  rrxcph  21029  ovoliunlem1  21118  ovoliunlem3  21120  ovoliun  21121  ovoliun2  21122  ovolscalem1  21129  volfiniun  21162  uniioombllem4  21200  mbfmptcl  21249  mbfeqalem  21254  mbfres2  21257  ismbf3d  21266  mbfsup  21276  mbfinf  21277  mbflim  21280  itg1ge0  21298  itg1mulc  21316  i1fposd  21319  itg1climres  21326  mbfi1fseqlem4  21330  itg2lea  21356  itg2splitlem  21360  itg2split  21361  itg2monolem1  21362  itg2mono  21365  itg2i1fseqle  21366  itg2i1fseq  21367  itg2addlem  21370  itg2cnlem1  21373  itgeqa  21425  itgss3  21426  itgfsum  21438  itgabs  21446  itggt0  21453  dvmptcl  21567  dvmptco  21580  dvlipcn  21600  dvle  21613  dvfsumle  21627  dvfsumge  21628  dvfsumabs  21629  dvmptrecl  21630  dvfsumlem2  21633  itgparts  21653  itgsubstlem  21654  itgsubst  21655  coeeulem  21826  dgrlem  21831  dgrlb  21838  coeaddlem  21850  coecj  21879  ulmss  21996  ulmdvlem2  22000  itgulm2  22008  logtayl  22239  leibpi  22471  xrlimcnp  22496  o1cxp  22502  jensen  22516  wilthlem2  22541  sqff1o  22654  fsumdvdscom  22659  fsumdvdsmul  22669  dchrmulcl  22722  dchrmulid2  22725  dchrinv  22734  dchrisumlem3  22874  dchrvmasumlem2  22881  ostth1  23016  tgtrisegint  23088  ercgrg  23106  f1otrg  23270  f1otrge  23271  elntg  23383  ubthlem2  24425  abrexss  26046  ofrn  26109  fmptcof2  26131  fcnvgreu  26143  disjdsct  26150  ressprs  26262  oduprs  26263  submarchi  26349  archiabl  26361  lmodslmd  26366  sumpr  26388  ordtrest2NEWlem  26498  lmdvg  26529  esumcl  26632  esumeq2d  26639  esumnul  26648  hasheuni  26680  esumcvg  26681  insiga  26726  measvunilem  26772  measvunilem0  26773  measdivcstOLD  26784  cntmeas  26786  voliune  26790  volfiniune  26791  1stmbfm  26820  2ndmbfm  26821  sitgf  26878  eulerpartlems  26888  eulerpartlemsv3  26889  eulerpartgbij  26900  eulerpartlemgvv  26904  sseqf  26920  dstrvprob  26999  signsvvfval  27124  lgambdd  27168  subfacp1lem3  27215  subfacp1lem5  27217  erdszelem8  27231  ptpcon  27267  rescon  27280  cvmliftmolem2  27316  cvmlift2lem11  27347  cvmliftphtlem  27351  fprod2dlem  27636  fin2so  28565  mblfinlem2  28578  itgabsnc  28610  itggt0cn  28613  prdsbnd  28841  prdstotbnd  28842  prdsbnd2  28843  rrnequiv  28883  fnwe2lem1  29552  rfcnnnub  29907  climinf  29928  climsuse  29930  stoweidlem5  29949  stoweidlem16  29960  stoweidlem21  29965  stoweidlem24  29968  stoweidlem25  29969  stoweidlem28  29972  stoweidlem31  29975  stoweidlem41  29985  stoweidlem42  29986  stoweidlem44  29988  stoweidlem45  29989  stoweidlem48  29992  stoweidlem51  29995  stoweidlem54  29998  stoweidlem57  30001  stoweidlem60  30004  stoweidlem62  30006  stirlinglem5  30022  gsumsmonply1  30996  gsummoncoe1  30997  cpmatmcllem  31208  bnj93  32189  bnj518  32212  bnj1489  32380  eqlkr3  33085  dih1dimatlem  35313
  Copyright terms: Public domain W3C validator