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

Theorem r19.21bi 2616
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 2523 . . . 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 2518
This theorem is referenced by:  rspec2  2617  rspec3  2618  r19.21be  2619  reusv6OLD  4517  ralxfr2d  4522  isoselem  5772  boxcutc  6827  xpf1o  6991  fineqvlem  7045  indexfi  7131  dffi3  7152  suppr  7187  supiso  7191  ordtypelem9  7209  brwdom3  7264  xpwdomg  7267  ixpiunwdom  7273  infxpenc2lem1  7614  hsmexlem4  8023  gchina  8289  wunom  8310  prcdnq  8585  prnmax  8587  monoord2  11044  seqshft  11546  limsupgre  11921  limsupbnd1  11922  limsupbnd2  11923  climmpt2  12013  rlimcld2  12018  rlimmptrcl  12047  lo1mptrcl  12061  o1mptrcl  12062  climsup  12109  fsum2dlem  12199  fsumiun  12245  iserodd  12851  vdwlem1  12991  vdwlem6  12996  vdwnnlem3  13007  imasvscafn  13402  fuciso  13812  evlfcl  13959  yonedalem3b  14016  yonedainv  14018  acsmapd  14244  prdsmndd  14368  dprdspan  15225  ablfaclem2  15284  issrngd  15589  psrbaglesupp  16077  psrbagcon  16080  psrass1lem  16086  evlslem2  16212  frgpcyg  16490  ordtrest2lem  16896  cncmp  17082  1stckgenlem  17211  ptcld  17270  dfac14  17275  txcnp  17277  ptcnplem  17278  ptcnp  17279  ptcn  17284  pthaus  17295  xkococnlem  17316  xkococn  17317  cnmpt11  17320  cnmpt1t  17322  cnmpt12  17324  cnmptkp  17337  cnmptk1  17338  cnmptkk  17340  cnmptk1p  17342  cnmptk2  17343  cnmpt2k  17345  xpstopnlem1  17463  cnpflfi  17657  ptcmplem2  17710  cnmpt1plusg  17733  cnmpt2plusg  17734  cnmpt1vsca  17839  cnmpt2vsca  17840  prdsxmetlem  17895  prdsbl  18000  prdsxmslem2  18038  cnmpt1ds  18310  cnmpt2ds  18311  cncfmpt2ss  18382  bndth  18419  cnmpt1ip  18637  cnmpt2ip  18638  iscmet3lem2  18681  ovoliunlem1  18824  ovoliunlem3  18826  ovoliun  18827  ovoliun2  18828  ovolscalem1  18835  volfiniun  18867  uniioombllem4  18904  mbfmptcl  18955  mbfeqalem  18960  mbfres2  18963  ismbf3d  18972  mbfsup  18982  mbfinf  18983  mbflim  18986  itg1ge0  19004  itg1mulc  19022  i1fposd  19025  itg1climres  19032  mbfi1fseqlem4  19036  itg2lea  19062  itg2splitlem  19066  itg2split  19067  itg2monolem1  19068  itg2mono  19071  itg2i1fseqle  19072  itg2i1fseq  19073  itg2addlem  19076  itg2cnlem1  19079  itgeqa  19131  itgss3  19132  itgfsum  19144  itgabs  19152  itggt0  19159  dvmptcl  19271  dvmptco  19284  dvlipcn  19304  dvle  19317  dvfsumle  19331  dvfsumge  19332  dvfsumabs  19333  dvmptrecl  19334  dvfsumlem2  19337  itgparts  19357  itgsubstlem  19358  itgsubst  19359  mpfind  19391  coeeulem  19569  dgrlem  19574  dgrlb  19581  coeaddlem  19593  coecj  19622  ulmss  19737  ulmdvlem2  19741  itgulm2  19748  logtayl  19970  leibpi  20201  xrlimcnp  20226  o1cxp  20232  jensen  20246  wilthlem2  20270  sqff1o  20383  fsumdvdscom  20388  fsumdvdsmul  20398  dchrmulcl  20451  dchrmulid2  20454  dchrinv  20463  dchrisumlem3  20603  dchrvmasumlem2  20610  ostth1  20745  ubthlem2  21411  abrexss  23002  subfacp1lem3  23086  subfacp1lem5  23088  erdszelem8  23102  ptpcon  23137  rescon  23150  cvmliftmolem2  23186  cvmlift2lem11  23217  cvmliftphtlem  23221  dedekind  23454  dedekindle  23455  supwlub  24642  prdsbnd  25885  prdstotbnd  25886  prdsbnd2  25887  rrnequiv  25927  fnwe2lem1  26515  frlmgsum  26600  uvcresum  26610  psgnunilem5  26785  climinf  27101  climsuse  27103  stoweidlem16  27134  stoweidlem21  27139  stoweidlem24  27142  stoweidlem31  27149  stoweidlem41  27159  stoweidlem42  27160  stoweidlem51  27169  stoweidlem57  27175  stoweidlem60  27178  stirlinglem5  27196  bnj93  28027  bnj518  28050  bnj1489  28218  eqlkr3  28541  dih1dimatlem  30769
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 2523
  Copyright terms: Public domain W3C validator