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

Theorem r19.21bi 2796
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 2702 . . . 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 1774 . 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 1549    e. wcel 1725   A.wral 2697
This theorem is referenced by:  rspec2  2797  rspec3  2798  r19.21be  2799  reusv6OLD  4726  ralxfr2d  4731  isoselem  6053  boxcutc  7097  xpf1o  7261  fineqvlem  7315  indexfi  7406  dffi3  7428  suppr  7465  supiso  7469  ordtypelem9  7487  brwdom3  7542  xpwdomg  7545  ixpiunwdom  7551  infxpenc2lem1  7892  hsmexlem4  8301  gchina  8566  wunom  8587  prcdnq  8862  prnmax  8864  monoord2  11346  seqshft  11892  limsupgre  12267  limsupbnd1  12268  limsupbnd2  12269  climmpt2  12359  rlimcld2  12364  rlimmptrcl  12393  lo1mptrcl  12407  o1mptrcl  12408  climsup  12455  fsum2dlem  12546  fsumiun  12592  iserodd  13201  vdwlem1  13341  vdwlem6  13346  vdwnnlem3  13357  imasvscafn  13754  fuciso  14164  evlfcl  14311  yonedainv  14370  acsmapd  14596  prdsmndd  14720  dprdspan  15577  ablfaclem2  15636  issrngd  15941  psrbaglesupp  16425  psrbagcon  16428  psrass1lem  16434  evlslem2  16560  frgpcyg  16846  neiptoptop  17187  neiptopnei  17188  ordtrest2lem  17259  cncmp  17447  1stckgenlem  17577  ptcld  17637  dfac14  17642  txcnp  17644  ptcnplem  17645  ptcnp  17646  ptcn  17651  pthaus  17662  xkococnlem  17683  xkococn  17684  cnmpt11  17687  cnmpt1t  17689  cnmpt12  17691  cnmptkp  17704  cnmptk1  17705  cnmptkk  17707  cnmptk1p  17709  cnmptk2  17710  cnmpt2k  17712  xpstopnlem1  17833  cnpflfi  18023  ptcmplem2  18076  cnextcn  18090  cnextfres  18091  cnmpt1plusg  18109  cnmpt2plusg  18110  cnmpt1vsca  18215  cnmpt2vsca  18216  ustfilxp  18234  utoptop  18256  restutop  18259  restutopopn  18260  ucncn  18307  cfilufg  18315  trcfilu  18316  psmet0  18331  psmettri2  18332  prdsxmetlem  18390  prdsbl  18513  prdsxmslem2  18551  metutopOLD  18604  psmetutop  18605  cnmpt1ds  18865  cnmpt2ds  18866  cncfmpt2ss  18937  bndth  18975  cnmpt1ip  19193  cnmpt2ip  19194  iscmet3lem2  19237  cmetcusp1OLD  19297  cmetcusp1  19298  ovoliunlem1  19390  ovoliunlem3  19392  ovoliun  19393  ovoliun2  19394  ovolscalem1  19401  volfiniun  19433  uniioombllem4  19470  mbfmptcl  19521  mbfeqalem  19526  mbfres2  19529  ismbf3d  19538  mbfsup  19548  mbfinf  19549  mbflim  19552  itg1ge0  19570  itg1mulc  19588  i1fposd  19591  itg1climres  19598  mbfi1fseqlem4  19602  itg2lea  19628  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2mono  19637  itg2i1fseqle  19638  itg2i1fseq  19639  itg2addlem  19642  itg2cnlem1  19645  itgeqa  19697  itgss3  19698  itgfsum  19710  itgabs  19718  itggt0  19725  dvmptcl  19837  dvmptco  19850  dvlipcn  19870  dvle  19883  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  dvmptrecl  19900  dvfsumlem2  19903  itgparts  19923  itgsubstlem  19924  itgsubst  19925  mpfind  19957  coeeulem  20135  dgrlem  20140  dgrlb  20147  coeaddlem  20159  coecj  20188  ulmss  20305  ulmdvlem2  20309  itgulm2  20317  logtayl  20543  leibpi  20774  xrlimcnp  20799  o1cxp  20805  jensen  20819  wilthlem2  20844  sqff1o  20957  fsumdvdscom  20962  fsumdvdsmul  20972  dchrmulcl  21025  dchrmulid2  21028  dchrinv  21037  dchrisumlem3  21177  dchrvmasumlem2  21184  ostth1  21319  ubthlem2  22365  abrexss  23985  ofrn  24044  fmptcof2  24068  disjdsct  24082  sumpr  24210  kerf1hrm  24254  lmdvg  24330  esumcl  24419  esumeq2d  24426  esumnul  24435  hasheuni  24467  esumcvg  24468  insiga  24512  measvunilem  24558  measvunilem0  24559  measdivcstOLD  24570  cntmeas  24572  voliune  24577  volfiniune  24578  1stmbfm  24602  2ndmbfm  24603  sitgf  24652  dstrvprob  24721  lgambdd  24813  subfacp1lem3  24860  subfacp1lem5  24862  erdszelem8  24876  ptpcon  24912  rescon  24925  cvmliftmolem2  24961  cvmlift2lem11  24992  cvmliftphtlem  24996  dedekind  25179  dedekindle  25180  fprod2dlem  25296  mblfinlem  26234  itgabsnc  26264  itggt0cn  26267  prdsbnd  26493  prdstotbnd  26494  prdsbnd2  26495  rrnequiv  26535  fnwe2lem1  27116  frlmgsum  27200  uvcresum  27210  psgnunilem5  27385  rfcnnnub  27674  climinf  27699  climsuse  27701  stoweidlem5  27721  stoweidlem16  27732  stoweidlem21  27737  stoweidlem24  27740  stoweidlem25  27741  stoweidlem28  27744  stoweidlem31  27747  stoweidlem41  27757  stoweidlem42  27758  stoweidlem44  27760  stoweidlem45  27761  stoweidlem48  27764  stoweidlem51  27767  stoweidlem54  27770  stoweidlem57  27773  stoweidlem60  27776  stoweidlem62  27778  stirlinglem5  27794  bnj93  29171  bnj518  29194  bnj1489  29362  eqlkr3  29836  dih1dimatlem  32064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2702
  Copyright terms: Public domain W3C validator