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

Theorem r19.21bi 2641
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 2548 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 188 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1794 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 418 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527    e. wcel 1684   A.wral 2543
This theorem is referenced by:  rspec2  2642  rspec3  2643  r19.21be  2644  reusv6OLD  4545  ralxfr2d  4550  isoselem  5838  boxcutc  6859  xpf1o  7023  fineqvlem  7077  indexfi  7163  dffi3  7184  suppr  7219  supiso  7223  ordtypelem9  7241  brwdom3  7296  xpwdomg  7299  ixpiunwdom  7305  infxpenc2lem1  7646  hsmexlem4  8055  gchina  8321  wunom  8342  prcdnq  8617  prnmax  8619  monoord2  11077  seqshft  11580  limsupgre  11955  limsupbnd1  11956  limsupbnd2  11957  climmpt2  12047  rlimcld2  12052  rlimmptrcl  12081  lo1mptrcl  12095  o1mptrcl  12096  climsup  12143  fsum2dlem  12233  fsumiun  12279  iserodd  12888  vdwlem1  13028  vdwlem6  13033  vdwnnlem3  13044  imasvscafn  13439  fuciso  13849  evlfcl  13996  yonedalem3b  14053  yonedainv  14055  acsmapd  14281  prdsmndd  14405  dprdspan  15262  ablfaclem2  15321  issrngd  15626  psrbaglesupp  16114  psrbagcon  16117  psrass1lem  16123  evlslem2  16249  frgpcyg  16527  ordtrest2lem  16933  cncmp  17119  1stckgenlem  17248  ptcld  17307  dfac14  17312  txcnp  17314  ptcnplem  17315  ptcnp  17316  ptcn  17321  pthaus  17332  xkococnlem  17353  xkococn  17354  cnmpt11  17357  cnmpt1t  17359  cnmpt12  17361  cnmptkp  17374  cnmptk1  17375  cnmptkk  17377  cnmptk1p  17379  cnmptk2  17380  cnmpt2k  17382  xpstopnlem1  17500  cnpflfi  17694  ptcmplem2  17747  cnmpt1plusg  17770  cnmpt2plusg  17771  cnmpt1vsca  17876  cnmpt2vsca  17877  prdsxmetlem  17932  prdsbl  18037  prdsxmslem2  18075  cnmpt1ds  18347  cnmpt2ds  18348  cncfmpt2ss  18419  bndth  18456  cnmpt1ip  18674  cnmpt2ip  18675  iscmet3lem2  18718  ovoliunlem1  18861  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovolscalem1  18872  volfiniun  18904  uniioombllem4  18941  mbfmptcl  18992  mbfeqalem  18997  mbfres2  19000  ismbf3d  19009  mbfsup  19019  mbfinf  19020  mbflim  19023  itg1ge0  19041  itg1mulc  19059  i1fposd  19062  itg1climres  19069  mbfi1fseqlem4  19073  itg2lea  19099  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2cnlem1  19116  itgeqa  19168  itgss3  19169  itgfsum  19181  itgabs  19189  itggt0  19196  dvmptcl  19308  dvmptco  19321  dvlipcn  19341  dvle  19354  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvmptrecl  19371  dvfsumlem2  19374  itgparts  19394  itgsubstlem  19395  itgsubst  19396  mpfind  19428  coeeulem  19606  dgrlem  19611  dgrlb  19618  coeaddlem  19630  coecj  19659  ulmss  19774  ulmdvlem2  19778  itgulm2  19785  logtayl  20007  leibpi  20238  xrlimcnp  20263  o1cxp  20269  jensen  20283  wilthlem2  20307  sqff1o  20420  fsumdvdscom  20425  fsumdvdsmul  20435  dchrmulcl  20488  dchrmulid2  20491  dchrinv  20500  dchrisumlem3  20640  dchrvmasumlem2  20647  ostth1  20782  ubthlem2  21450  abrexss  23040  sumpr  23168  ofrn  23206  fmptcof2  23229  disjdsct  23369  lmdvg  23376  esumcl  23413  esumeq2d  23419  esumnul  23427  hasheuni  23453  esumcvg  23454  ofcfval4  23466  insiga  23498  measvunilem  23540  measvunilem0  23541  measdivcstOLD  23551  measdivcst  23552  cntmeas  23553  1stmbfm  23565  2ndmbfm  23566  imambfm  23567  itgmeq123dTMP  23589  dstrvprob  23672  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem8  23729  ptpcon  23764  rescon  23777  cvmliftmolem2  23813  cvmlift2lem11  23844  cvmliftphtlem  23848  dedekind  24082  dedekindle  24083  supwlub  25274  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  rrnequiv  26559  fnwe2lem1  27147  frlmgsum  27232  uvcresum  27242  psgnunilem5  27417  climinf  27732  climsuse  27734  stoweidlem16  27765  stoweidlem21  27770  stoweidlem24  27773  stoweidlem31  27780  stoweidlem41  27790  stoweidlem42  27791  stoweidlem51  27800  stoweidlem57  27806  stoweidlem60  27809  stirlinglem5  27827  bnj93  28895  bnj518  28918  bnj1489  29086  eqlkr3  29291  dih1dimatlem  31519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2548
  Copyright terms: Public domain W3C validator