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

Theorem r19.21bi 2740
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 2647 . . . 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 1766 . 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 1546    e. wcel 1717   A.wral 2642
This theorem is referenced by:  rspec2  2741  rspec3  2742  r19.21be  2743  reusv6OLD  4667  ralxfr2d  4672  isoselem  5993  boxcutc  7034  xpf1o  7198  fineqvlem  7252  indexfi  7342  dffi3  7364  suppr  7399  supiso  7403  ordtypelem9  7421  brwdom3  7476  xpwdomg  7479  ixpiunwdom  7485  infxpenc2lem1  7826  hsmexlem4  8235  gchina  8500  wunom  8521  prcdnq  8796  prnmax  8798  monoord2  11274  seqshft  11820  limsupgre  12195  limsupbnd1  12196  limsupbnd2  12197  climmpt2  12287  rlimcld2  12292  rlimmptrcl  12321  lo1mptrcl  12335  o1mptrcl  12336  climsup  12383  fsum2dlem  12474  fsumiun  12520  iserodd  13129  vdwlem1  13269  vdwlem6  13274  vdwnnlem3  13285  imasvscafn  13682  fuciso  14092  evlfcl  14239  yonedainv  14298  acsmapd  14524  prdsmndd  14648  dprdspan  15505  ablfaclem2  15564  issrngd  15869  psrbaglesupp  16353  psrbagcon  16356  psrass1lem  16362  evlslem2  16488  frgpcyg  16770  neiptoptop  17111  neiptopnei  17112  ordtrest2lem  17182  cncmp  17370  1stckgenlem  17499  ptcld  17559  dfac14  17564  txcnp  17566  ptcnplem  17567  ptcnp  17568  ptcn  17573  pthaus  17584  xkococnlem  17605  xkococn  17606  cnmpt11  17609  cnmpt1t  17611  cnmpt12  17613  cnmptkp  17626  cnmptk1  17627  cnmptkk  17629  cnmptk1p  17631  cnmptk2  17632  cnmpt2k  17634  xpstopnlem1  17755  cnpflfi  17945  ptcmplem2  17998  cnextcn  18012  cnextfres  18013  cnmpt1plusg  18031  cnmpt2plusg  18032  cnmpt1vsca  18137  cnmpt2vsca  18138  ustfilxp  18156  utoptop  18178  restutop  18181  restutopopn  18182  ucncn  18229  cfilufg  18237  trcfilu  18238  prdsxmetlem  18299  prdsbl  18404  prdsxmslem2  18442  metutop  18480  cnmpt1ds  18737  cnmpt2ds  18738  cncfmpt2ss  18809  bndth  18847  cnmpt1ip  19065  cnmpt2ip  19066  iscmet3lem2  19109  cmetcusp1  19167  ovoliunlem1  19258  ovoliunlem3  19260  ovoliun  19261  ovoliun2  19262  ovolscalem1  19269  volfiniun  19301  uniioombllem4  19338  mbfmptcl  19389  mbfeqalem  19394  mbfres2  19397  ismbf3d  19406  mbfsup  19416  mbfinf  19417  mbflim  19420  itg1ge0  19438  itg1mulc  19456  i1fposd  19459  itg1climres  19466  mbfi1fseqlem4  19470  itg2lea  19496  itg2splitlem  19500  itg2split  19501  itg2monolem1  19502  itg2mono  19505  itg2i1fseqle  19506  itg2i1fseq  19507  itg2addlem  19510  itg2cnlem1  19513  itgeqa  19565  itgss3  19566  itgfsum  19578  itgabs  19586  itggt0  19593  dvmptcl  19705  dvmptco  19718  dvlipcn  19738  dvle  19751  dvfsumle  19765  dvfsumge  19766  dvfsumabs  19767  dvmptrecl  19768  dvfsumlem2  19771  itgparts  19791  itgsubstlem  19792  itgsubst  19793  mpfind  19825  coeeulem  20003  dgrlem  20008  dgrlb  20015  coeaddlem  20027  coecj  20056  ulmss  20173  ulmdvlem2  20177  itgulm2  20185  logtayl  20411  leibpi  20642  xrlimcnp  20667  o1cxp  20673  jensen  20687  wilthlem2  20712  sqff1o  20825  fsumdvdscom  20830  fsumdvdsmul  20840  dchrmulcl  20893  dchrmulid2  20896  dchrinv  20905  dchrisumlem3  21045  dchrvmasumlem2  21052  ostth1  21187  ubthlem2  22214  abrexss  23830  fmptcof2  23911  disjdsct  23924  sumpr  24040  kerf1hrm  24071  lmdvg  24135  esumcl  24216  esumeq2d  24223  esumnul  24232  hasheuni  24264  esumcvg  24265  insiga  24309  measvunilem  24353  measvunilem0  24354  measdivcstOLD  24365  cntmeas  24367  voliune  24372  volfiniune  24373  1stmbfm  24397  2ndmbfm  24398  dstrvprob  24501  lgambdd  24593  subfacp1lem3  24640  subfacp1lem5  24642  erdszelem8  24656  ptpcon  24692  rescon  24705  cvmliftmolem2  24741  cvmlift2lem11  24772  cvmliftphtlem  24776  dedekind  24959  dedekindle  24960  itgabsnc  25967  itggt0cn  25970  prdsbnd  26186  prdstotbnd  26187  prdsbnd2  26188  rrnequiv  26228  fnwe2lem1  26809  frlmgsum  26894  uvcresum  26904  psgnunilem5  27079  rfcnnnub  27368  climinf  27393  climsuse  27395  stoweidlem5  27415  stoweidlem16  27426  stoweidlem21  27431  stoweidlem24  27434  stoweidlem25  27435  stoweidlem28  27438  stoweidlem31  27441  stoweidlem41  27451  stoweidlem42  27452  stoweidlem44  27454  stoweidlem45  27455  stoweidlem48  27458  stoweidlem51  27461  stoweidlem54  27464  stoweidlem57  27467  stoweidlem60  27470  stoweidlem62  27472  stirlinglem5  27488  bnj93  28565  bnj518  28588  bnj1489  28756  eqlkr3  29267  dih1dimatlem  31495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2647
  Copyright terms: Public domain W3C validator