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

Theorem r19.21bi 2804
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 2710 . . . 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 1803 . 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 1360    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-ral 2710
This theorem is referenced by:  rspec2  2805  rspec3  2806  r19.21be  2807  reusv6OLD  4491  ralxfr2d  4496  f1oresrab  5862  isoselem  6019  boxcutc  7294  xpf1o  7461  fineqvlem  7515  indexfi  7607  dffi3  7669  suppr  7706  supiso  7710  ordtypelem9  7728  brwdom3  7785  xpwdomg  7788  ixpiunwdom  7794  infxpenc2lem1  8173  hsmexlem4  8586  gchina  8854  wunom  8875  prcdnq  9150  prnmax  9152  dedekind  9521  dedekindle  9522  monoord2  11821  seqshft  12558  limsupgre  12943  limsupbnd1  12944  limsupbnd2  12945  climmpt2  13035  rlimcld2  13040  rlimmptrcl  13069  lo1mptrcl  13083  o1mptrcl  13084  climsup  13131  fsum2dlem  13221  fsumiun  13267  iserodd  13885  vdwlem1  14025  vdwlem6  14030  vdwnnlem3  14041  imasvscafn  14458  fuciso  14868  evlfcl  15015  yonedainv  15074  acsmapd  15331  prdsmndd  15437  psgnunilem5  15980  dprdspan  16498  ablfaclem2  16561  issrngd  16870  psrbaglesupp  17369  psrbaglesuppOLD  17370  psrbagcon  17374  psrass1lem  17381  evlslem2  17525  frgpcyg  17848  frlmgsumOLD  18037  frlmgsum  18038  uvcresum  18060  neiptoptop  18577  neiptopnei  18578  ordtrest2lem  18649  cncmp  18837  1stckgenlem  18968  ptcld  19028  dfac14  19033  txcnp  19035  ptcnplem  19036  ptcnp  19037  ptcn  19042  pthaus  19053  xkococnlem  19074  xkococn  19075  cnmpt11  19078  cnmpt1t  19080  cnmpt12  19082  cnmptkp  19095  cnmptk1  19096  cnmptkk  19098  cnmptk1p  19100  cnmptk2  19101  cnmpt2k  19103  xpstopnlem1  19224  cnpflfi  19414  ptcmplem2  19467  cnextcn  19481  cnextfres  19482  cnmpt1plusg  19500  cnmpt2plusg  19501  cnmpt1vsca  19610  cnmpt2vsca  19611  ustfilxp  19629  utoptop  19651  restutop  19654  restutopopn  19655  ucncn  19702  cfilufg  19710  trcfilu  19711  psmet0  19726  psmettri2  19727  prdsxmetlem  19785  prdsbl  19908  prdsxmslem2  19946  metutopOLD  19999  psmetutop  20000  cnmpt1ds  20261  cnmpt2ds  20262  cncfmpt2ss  20333  bndth  20372  cnmpt1ip  20601  cnmpt2ip  20602  iscmet3lem2  20645  cmetcusp1OLD  20705  cmetcusp1  20706  rrxcph  20738  ovoliunlem1  20827  ovoliunlem3  20829  ovoliun  20830  ovoliun2  20831  ovolscalem1  20838  volfiniun  20870  uniioombllem4  20908  mbfmptcl  20957  mbfeqalem  20962  mbfres2  20965  ismbf3d  20974  mbfsup  20984  mbfinf  20985  mbflim  20988  itg1ge0  21006  itg1mulc  21024  i1fposd  21027  itg1climres  21034  mbfi1fseqlem4  21038  itg2lea  21064  itg2splitlem  21068  itg2split  21069  itg2monolem1  21070  itg2mono  21073  itg2i1fseqle  21074  itg2i1fseq  21075  itg2addlem  21078  itg2cnlem1  21081  itgeqa  21133  itgss3  21134  itgfsum  21146  itgabs  21154  itggt0  21161  dvmptcl  21275  dvmptco  21288  dvlipcn  21308  dvle  21321  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvmptrecl  21338  dvfsumlem2  21341  itgparts  21361  itgsubstlem  21362  itgsubst  21363  mpfind  21396  coeeulem  21577  dgrlem  21582  dgrlb  21589  coeaddlem  21601  coecj  21630  ulmss  21747  ulmdvlem2  21751  itgulm2  21759  logtayl  21990  leibpi  22222  xrlimcnp  22247  o1cxp  22253  jensen  22267  wilthlem2  22292  sqff1o  22405  fsumdvdscom  22410  fsumdvdsmul  22420  dchrmulcl  22473  dchrmulid2  22476  dchrinv  22485  dchrisumlem3  22625  dchrvmasumlem2  22632  ostth1  22767  tgtrisegint  22834  ercgrg  22850  f1otrg  22940  f1otrge  22941  elntg  23053  ubthlem2  24095  abrexss  25717  ofrn  25781  fmptcof2  25803  fcnvgreu  25815  disjdsct  25822  ressprs  25939  oduprs  25940  submarchi  26027  archiabl  26039  srgi  26047  srgrz  26061  lmodslmd  26069  sumpr  26091  kerf1hrm  26145  ordtrest2NEWlem  26206  lmdvg  26237  esumcl  26340  esumeq2d  26347  esumnul  26356  hasheuni  26388  esumcvg  26389  insiga  26434  measvunilem  26480  measvunilem0  26481  measdivcstOLD  26492  cntmeas  26494  voliune  26499  volfiniune  26500  1stmbfm  26529  2ndmbfm  26530  sitgf  26581  eulerpartlems  26591  eulerpartlemsv3  26592  eulerpartlemgvv  26607  sseqf  26623  dstrvprob  26702  signsvvfval  26827  lgambdd  26871  subfacp1lem3  26918  subfacp1lem5  26920  erdszelem8  26934  ptpcon  26970  rescon  26983  cvmliftmolem2  27019  cvmlift2lem11  27050  cvmliftphtlem  27054  fprod2dlem  27338  fin2so  28260  mblfinlem2  28273  itgabsnc  28305  itggt0cn  28308  prdsbnd  28536  prdstotbnd  28537  prdsbnd2  28538  rrnequiv  28578  fnwe2lem1  29248  rfcnnnub  29603  climinf  29625  climsuse  29627  stoweidlem5  29646  stoweidlem16  29657  stoweidlem21  29662  stoweidlem24  29665  stoweidlem25  29666  stoweidlem28  29669  stoweidlem31  29672  stoweidlem41  29682  stoweidlem42  29683  stoweidlem44  29685  stoweidlem45  29686  stoweidlem48  29689  stoweidlem51  29692  stoweidlem54  29695  stoweidlem57  29698  stoweidlem60  29701  stoweidlem62  29703  stirlinglem5  29719  bnj93  31558  bnj518  31581  bnj1489  31749  eqlkr3  32319  dih1dimatlem  34547
  Copyright terms: Public domain W3C validator