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

Theorem r19.21bi 2654
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 2561 . . . 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 1806 . 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 1530    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rspec2  2655  rspec3  2656  r19.21be  2657  reusv6OLD  4561  ralxfr2d  4566  isoselem  5854  boxcutc  6875  xpf1o  7039  fineqvlem  7093  indexfi  7179  dffi3  7200  suppr  7235  supiso  7239  ordtypelem9  7257  brwdom3  7312  xpwdomg  7315  ixpiunwdom  7321  infxpenc2lem1  7662  hsmexlem4  8071  gchina  8337  wunom  8358  prcdnq  8633  prnmax  8635  monoord2  11093  seqshft  11596  limsupgre  11971  limsupbnd1  11972  limsupbnd2  11973  climmpt2  12063  rlimcld2  12068  rlimmptrcl  12097  lo1mptrcl  12111  o1mptrcl  12112  climsup  12159  fsum2dlem  12249  fsumiun  12295  iserodd  12904  vdwlem1  13044  vdwlem6  13049  vdwnnlem3  13060  imasvscafn  13455  fuciso  13865  evlfcl  14012  yonedalem3b  14069  yonedainv  14071  acsmapd  14297  prdsmndd  14421  dprdspan  15278  ablfaclem2  15337  issrngd  15642  psrbaglesupp  16130  psrbagcon  16133  psrass1lem  16139  evlslem2  16265  frgpcyg  16543  ordtrest2lem  16949  cncmp  17135  1stckgenlem  17264  ptcld  17323  dfac14  17328  txcnp  17330  ptcnplem  17331  ptcnp  17332  ptcn  17337  pthaus  17348  xkococnlem  17369  xkococn  17370  cnmpt11  17373  cnmpt1t  17375  cnmpt12  17377  cnmptkp  17390  cnmptk1  17391  cnmptkk  17393  cnmptk1p  17395  cnmptk2  17396  cnmpt2k  17398  xpstopnlem1  17516  cnpflfi  17710  ptcmplem2  17763  cnmpt1plusg  17786  cnmpt2plusg  17787  cnmpt1vsca  17892  cnmpt2vsca  17893  prdsxmetlem  17948  prdsbl  18053  prdsxmslem2  18091  cnmpt1ds  18363  cnmpt2ds  18364  cncfmpt2ss  18435  bndth  18472  cnmpt1ip  18690  cnmpt2ip  18691  iscmet3lem2  18734  ovoliunlem1  18877  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  ovolscalem1  18888  volfiniun  18920  uniioombllem4  18957  mbfmptcl  19008  mbfeqalem  19013  mbfres2  19016  ismbf3d  19025  mbfsup  19035  mbfinf  19036  mbflim  19039  itg1ge0  19057  itg1mulc  19075  i1fposd  19078  itg1climres  19085  mbfi1fseqlem4  19089  itg2lea  19115  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2cnlem1  19132  itgeqa  19184  itgss3  19185  itgfsum  19197  itgabs  19205  itggt0  19212  dvmptcl  19324  dvmptco  19337  dvlipcn  19357  dvle  19370  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvmptrecl  19387  dvfsumlem2  19390  itgparts  19410  itgsubstlem  19411  itgsubst  19412  mpfind  19444  coeeulem  19622  dgrlem  19627  dgrlb  19634  coeaddlem  19646  coecj  19675  ulmss  19790  ulmdvlem2  19794  itgulm2  19801  logtayl  20023  leibpi  20254  xrlimcnp  20279  o1cxp  20285  jensen  20299  wilthlem2  20323  sqff1o  20436  fsumdvdscom  20441  fsumdvdsmul  20451  dchrmulcl  20504  dchrmulid2  20507  dchrinv  20516  dchrisumlem3  20656  dchrvmasumlem2  20663  ostth1  20798  ubthlem2  21466  abrexss  23056  sumpr  23184  ofrn  23221  fmptcof2  23244  disjdsct  23384  lmdvg  23391  esumcl  23428  esumeq2d  23434  esumnul  23442  hasheuni  23468  esumcvg  23469  ofcfval4  23481  insiga  23513  measvunilem  23555  measvunilem0  23556  measdivcstOLD  23566  measdivcst  23567  cntmeas  23568  1stmbfm  23580  2ndmbfm  23581  imambfm  23582  itgmeq123dTMP  23604  dstrvprob  23687  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem8  23744  ptpcon  23779  rescon  23792  cvmliftmolem2  23828  cvmlift2lem11  23859  cvmliftphtlem  23863  dedekind  24097  dedekindle  24098  itgabsnc  25020  itggt0cn  25023  supwlub  25377  prdsbnd  26620  prdstotbnd  26621  prdsbnd2  26622  rrnequiv  26662  fnwe2lem1  27250  frlmgsum  27335  uvcresum  27345  psgnunilem5  27520  climinf  27835  climsuse  27837  stoweidlem16  27868  stoweidlem21  27873  stoweidlem24  27876  stoweidlem31  27883  stoweidlem41  27893  stoweidlem42  27894  stoweidlem51  27903  stoweidlem57  27909  stoweidlem60  27912  stirlinglem5  27930  bnj93  29211  bnj518  29234  bnj1489  29402  eqlkr3  29913  dih1dimatlem  32141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2561
  Copyright terms: Public domain W3C validator