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

Theorem r19.21bi 2603
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 2513 . . . 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 2509
This theorem is referenced by:  rspec2  2604  rspec3  2605  r19.21be  2606  reusv6OLD  4436  ralxfr2d  4441  isoselem  5690  boxcutc  6745  xpf1o  6908  fineqvlem  6962  indexfi  7047  dffi3  7068  suppr  7103  supiso  7107  ordtypelem9  7125  brwdom3  7180  xpwdomg  7183  ixpiunwdom  7189  infxpenc2lem1  7530  hsmexlem4  7939  gchina  8201  wunom  8222  prcdnq  8497  prnmax  8499  monoord2  10955  seqshft  11457  limsupgre  11832  limsupbnd1  11833  limsupbnd2  11834  climmpt2  11924  rlimcld2  11929  rlimmptrcl  11958  lo1mptrcl  11972  o1mptrcl  11973  climsup  12020  fsum2dlem  12110  fsumiun  12156  iserodd  12762  vdwlem1  12902  vdwlem6  12907  vdwnnlem3  12918  imasvscafn  13313  fuciso  13693  evlfcl  13840  yonedalem3b  13897  yonedainv  13899  prdsmndd  14240  dprdspan  15097  ablfaclem2  15156  issrngd  15461  psrbaglesupp  15946  psrbagcon  15949  psrass1lem  15955  evlslem2  16081  frgpcyg  16359  ordtrest2lem  16765  cncmp  16951  1stckgenlem  17080  ptcld  17139  dfac14  17144  txcnp  17146  ptcnplem  17147  ptcnp  17148  ptcn  17153  pthaus  17164  xkococnlem  17185  xkococn  17186  cnmpt11  17189  cnmpt1t  17191  cnmpt12  17193  cnmptkp  17206  cnmptk1  17207  cnmptkk  17209  cnmptk1p  17211  cnmptk2  17212  cnmpt2k  17214  xpstopnlem1  17332  cnpflfi  17526  ptcmplem2  17579  cnmpt1plusg  17602  cnmpt2plusg  17603  cnmpt1vsca  17708  cnmpt2vsca  17709  prdsxmetlem  17764  prdsbl  17869  prdsxmslem2  17907  cnmpt1ds  18179  cnmpt2ds  18180  cncfmpt2ss  18251  bndth  18288  cnmpt1ip  18506  cnmpt2ip  18507  iscmet3lem2  18550  ovoliunlem1  18693  ovoliunlem3  18695  ovoliun  18696  ovoliun2  18697  ovolscalem1  18704  volfiniun  18736  uniioombllem4  18773  mbfmptcl  18824  mbfeqalem  18829  mbfres2  18832  ismbf3d  18841  mbfsup  18851  mbfinf  18852  mbflim  18855  itg1ge0  18873  itg1mulc  18891  i1fposd  18894  itg1climres  18901  mbfi1fseqlem4  18905  itg2lea  18931  itg2splitlem  18935  itg2split  18936  itg2monolem1  18937  itg2mono  18940  itg2i1fseqle  18941  itg2i1fseq  18942  itg2addlem  18945  itg2cnlem1  18948  itgeqa  19000  itgss3  19001  itgfsum  19013  itgabs  19021  itggt0  19028  dvmptcl  19140  dvmptco  19153  dvlipcn  19173  dvle  19186  dvfsumle  19200  dvfsumge  19201  dvfsumabs  19202  dvmptrecl  19203  dvfsumlem2  19206  itgparts  19226  itgsubstlem  19227  itgsubst  19228  mpfind  19260  coeeulem  19438  dgrlem  19443  dgrlb  19450  coeaddlem  19462  coecj  19491  ulmss  19606  ulmdvlem2  19610  itgulm2  19617  logtayl  19839  leibpi  20070  xrlimcnp  20095  o1cxp  20101  jensen  20115  wilthlem2  20139  sqff1o  20252  fsumdvdscom  20257  fsumdvdsmul  20267  dchrmulcl  20320  dchrmulid2  20323  dchrinv  20332  dchrisumlem3  20472  dchrvmasumlem2  20479  ostth1  20614  ubthlem2  21280  subfacp1lem3  22884  subfacp1lem5  22886  erdszelem8  22900  ptpcon  22935  rescon  22948  cvmliftmolem2  22984  cvmlift2lem11  23015  cvmliftphtlem  23019  dedekind  23252  dedekindle  23253  supwlub  24440  prdsbnd  25683  prdstotbnd  25684  prdsbnd2  25685  rrnequiv  25725  fnwe2lem1  26313  frlmgsum  26398  uvcresum  26408  psgnunilem5  26583  bnj93  27584  bnj518  27607  bnj1489  27775  eqlkr3  27980  dih1dimatlem  30208
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 2513
  Copyright terms: Public domain W3C validator