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

Theorem r19.21bi 2612
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 2520 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 190 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1774 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 420 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   A.wal 1532    e. wcel 1621   A.wral 2516
This theorem is referenced by:  rspec2  2613  rspec3  2614  r19.21be  2615  reusv6OLD  4482  ralxfr2d  4487  isoselem  5737  boxcutc  6792  xpf1o  6956  fineqvlem  7010  indexfi  7096  dffi3  7117  suppr  7152  supiso  7156  ordtypelem9  7174  brwdom3  7229  xpwdomg  7232  ixpiunwdom  7238  infxpenc2lem1  7579  hsmexlem4  7988  gchina  8254  wunom  8275  prcdnq  8550  prnmax  8552  monoord2  11008  seqshft  11510  limsupgre  11885  limsupbnd1  11886  limsupbnd2  11887  climmpt2  11977  rlimcld2  11982  rlimmptrcl  12011  lo1mptrcl  12025  o1mptrcl  12026  climsup  12073  fsum2dlem  12163  fsumiun  12209  iserodd  12815  vdwlem1  12955  vdwlem6  12960  vdwnnlem3  12971  imasvscafn  13366  fuciso  13776  evlfcl  13923  yonedalem3b  13980  yonedainv  13982  acsmapd  14208  prdsmndd  14332  dprdspan  15189  ablfaclem2  15248  issrngd  15553  psrbaglesupp  16041  psrbagcon  16044  psrass1lem  16050  evlslem2  16176  frgpcyg  16454  ordtrest2lem  16860  cncmp  17046  1stckgenlem  17175  ptcld  17234  dfac14  17239  txcnp  17241  ptcnplem  17242  ptcnp  17243  ptcn  17248  pthaus  17259  xkococnlem  17280  xkococn  17281  cnmpt11  17284  cnmpt1t  17286  cnmpt12  17288  cnmptkp  17301  cnmptk1  17302  cnmptkk  17304  cnmptk1p  17306  cnmptk2  17307  cnmpt2k  17309  xpstopnlem1  17427  cnpflfi  17621  ptcmplem2  17674  cnmpt1plusg  17697  cnmpt2plusg  17698  cnmpt1vsca  17803  cnmpt2vsca  17804  prdsxmetlem  17859  prdsbl  17964  prdsxmslem2  18002  cnmpt1ds  18274  cnmpt2ds  18275  cncfmpt2ss  18346  bndth  18383  cnmpt1ip  18601  cnmpt2ip  18602  iscmet3lem2  18645  ovoliunlem1  18788  ovoliunlem3  18790  ovoliun  18791  ovoliun2  18792  ovolscalem1  18799  volfiniun  18831  uniioombllem4  18868  mbfmptcl  18919  mbfeqalem  18924  mbfres2  18927  ismbf3d  18936  mbfsup  18946  mbfinf  18947  mbflim  18950  itg1ge0  18968  itg1mulc  18986  i1fposd  18989  itg1climres  18996  mbfi1fseqlem4  19000  itg2lea  19026  itg2splitlem  19030  itg2split  19031  itg2monolem1  19032  itg2mono  19035  itg2i1fseqle  19036  itg2i1fseq  19037  itg2addlem  19040  itg2cnlem1  19043  itgeqa  19095  itgss3  19096  itgfsum  19108  itgabs  19116  itggt0  19123  dvmptcl  19235  dvmptco  19248  dvlipcn  19268  dvle  19281  dvfsumle  19295  dvfsumge  19296  dvfsumabs  19297  dvmptrecl  19298  dvfsumlem2  19301  itgparts  19321  itgsubstlem  19322  itgsubst  19323  mpfind  19355  coeeulem  19533  dgrlem  19538  dgrlb  19545  coeaddlem  19557  coecj  19586  ulmss  19701  ulmdvlem2  19705  itgulm2  19712  logtayl  19934  leibpi  20165  xrlimcnp  20190  o1cxp  20196  jensen  20210  wilthlem2  20234  sqff1o  20347  fsumdvdscom  20352  fsumdvdsmul  20362  dchrmulcl  20415  dchrmulid2  20418  dchrinv  20427  dchrisumlem3  20567  dchrvmasumlem2  20574  ostth1  20709  ubthlem2  21375  abrexss  22966  subfacp1lem3  23050  subfacp1lem5  23052  erdszelem8  23066  ptpcon  23101  rescon  23114  cvmliftmolem2  23150  cvmlift2lem11  23181  cvmliftphtlem  23185  dedekind  23418  dedekindle  23419  supwlub  24606  prdsbnd  25849  prdstotbnd  25850  prdsbnd2  25851  rrnequiv  25891  fnwe2lem1  26479  frlmgsum  26564  uvcresum  26574  psgnunilem5  26749  stoweidlem16  27065  stoweidlem21  27070  stoweidlem24  27073  stoweidlem31  27080  stoweidlem41  27090  stoweidlem42  27091  stoweidlem51  27100  stoweidlem57  27106  stoweidlem60  27109  bnj93  27907  bnj518  27930  bnj1489  28098  eqlkr3  28421  dih1dimatlem  30649
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ral 2520
  Copyright terms: Public domain W3C validator