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

Theorem r19.21bi 2642
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 2549 . . . 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 1796 . 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 1685   A.wral 2544
This theorem is referenced by:  rspec2  2643  rspec3  2644  r19.21be  2645  reusv6OLD  4544  ralxfr2d  4549  isoselem  5800  boxcutc  6855  xpf1o  7019  fineqvlem  7073  indexfi  7159  dffi3  7180  suppr  7215  supiso  7219  ordtypelem9  7237  brwdom3  7292  xpwdomg  7295  ixpiunwdom  7301  infxpenc2lem1  7642  hsmexlem4  8051  gchina  8317  wunom  8338  prcdnq  8613  prnmax  8615  monoord2  11073  seqshft  11576  limsupgre  11951  limsupbnd1  11952  limsupbnd2  11953  climmpt2  12043  rlimcld2  12048  rlimmptrcl  12077  lo1mptrcl  12091  o1mptrcl  12092  climsup  12139  fsum2dlem  12229  fsumiun  12275  iserodd  12884  vdwlem1  13024  vdwlem6  13029  vdwnnlem3  13040  imasvscafn  13435  fuciso  13845  evlfcl  13992  yonedalem3b  14049  yonedainv  14051  acsmapd  14277  prdsmndd  14401  dprdspan  15258  ablfaclem2  15317  issrngd  15622  psrbaglesupp  16110  psrbagcon  16113  psrass1lem  16119  evlslem2  16245  frgpcyg  16523  ordtrest2lem  16929  cncmp  17115  1stckgenlem  17244  ptcld  17303  dfac14  17308  txcnp  17310  ptcnplem  17311  ptcnp  17312  ptcn  17317  pthaus  17328  xkococnlem  17349  xkococn  17350  cnmpt11  17353  cnmpt1t  17355  cnmpt12  17357  cnmptkp  17370  cnmptk1  17371  cnmptkk  17373  cnmptk1p  17375  cnmptk2  17376  cnmpt2k  17378  xpstopnlem1  17496  cnpflfi  17690  ptcmplem2  17743  cnmpt1plusg  17766  cnmpt2plusg  17767  cnmpt1vsca  17872  cnmpt2vsca  17873  prdsxmetlem  17928  prdsbl  18033  prdsxmslem2  18071  cnmpt1ds  18343  cnmpt2ds  18344  cncfmpt2ss  18415  bndth  18452  cnmpt1ip  18670  cnmpt2ip  18671  iscmet3lem2  18714  ovoliunlem1  18857  ovoliunlem3  18859  ovoliun  18860  ovoliun2  18861  ovolscalem1  18868  volfiniun  18900  uniioombllem4  18937  mbfmptcl  18988  mbfeqalem  18993  mbfres2  18996  ismbf3d  19005  mbfsup  19015  mbfinf  19016  mbflim  19019  itg1ge0  19037  itg1mulc  19055  i1fposd  19058  itg1climres  19065  mbfi1fseqlem4  19069  itg2lea  19095  itg2splitlem  19099  itg2split  19100  itg2monolem1  19101  itg2mono  19104  itg2i1fseqle  19105  itg2i1fseq  19106  itg2addlem  19109  itg2cnlem1  19112  itgeqa  19164  itgss3  19165  itgfsum  19177  itgabs  19185  itggt0  19192  dvmptcl  19304  dvmptco  19317  dvlipcn  19337  dvle  19350  dvfsumle  19364  dvfsumge  19365  dvfsumabs  19366  dvmptrecl  19367  dvfsumlem2  19370  itgparts  19390  itgsubstlem  19391  itgsubst  19392  mpfind  19424  coeeulem  19602  dgrlem  19607  dgrlb  19614  coeaddlem  19626  coecj  19655  ulmss  19770  ulmdvlem2  19774  itgulm2  19781  logtayl  20003  leibpi  20234  xrlimcnp  20259  o1cxp  20265  jensen  20279  wilthlem2  20303  sqff1o  20416  fsumdvdscom  20421  fsumdvdsmul  20431  dchrmulcl  20484  dchrmulid2  20487  dchrinv  20496  dchrisumlem3  20636  dchrvmasumlem2  20643  ostth1  20778  ubthlem2  21444  abrexss  23036  subfacp1lem3  23120  subfacp1lem5  23122  erdszelem8  23136  ptpcon  23171  rescon  23184  cvmliftmolem2  23220  cvmlift2lem11  23251  cvmliftphtlem  23255  dedekind  23488  dedekindle  23489  supwlub  24685  prdsbnd  25928  prdstotbnd  25929  prdsbnd2  25930  rrnequiv  25970  fnwe2lem1  26558  frlmgsum  26643  uvcresum  26653  psgnunilem5  26828  climinf  27143  climsuse  27145  stoweidlem16  27176  stoweidlem21  27181  stoweidlem24  27184  stoweidlem31  27191  stoweidlem41  27201  stoweidlem42  27202  stoweidlem51  27211  stoweidlem57  27217  stoweidlem60  27220  stirlinglem5  27238  bnj93  28174  bnj518  28197  bnj1489  28365  eqlkr3  28570  dih1dimatlem  30798
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 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2549
  Copyright terms: Public domain W3C validator