MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimivw Structured version   Visualization version   Unicode version

Theorem ralrimivw 2802
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
ralrimivw.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralrimivw  |-  ( ph  ->  A. x  e.  A  ps )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3  |-  ( ph  ->  ps )
21a1d 26 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2799 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1886   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757
This theorem depends on definitions:  df-bi 189  df-ral 2741
This theorem is referenced by:  2rmorex  3243  riinrab  4353  exse  4797  dmxp  5052  mpt2eq12  6348  ovmpt3rabdm  6523  offveqb  6550  exse2  6729  xpexgALT  6783  mpt2exg  6865  uniqs  7420  boxriin  7561  fisupg  7816  supmaxlemOLD  7979  fisup2g  7981  fisupcl  7982  fiinfg  8012  fiinf2g  8013  ordtypelem8  8037  wemapso2  8065  cantnflem1  8191  r1val1  8254  scottex  8353  dfac12k  8574  compssiso  8801  axcclem  8884  ondomon  8985  tskuni  9205  pinq  9349  supexpr  9476  dedekind  9794  supadd  10572  supmullem2  10575  zsupss  11250  qextlt  11493  qextle  11494  xrsupsslem  11589  xrinfmsslem  11590  supxrpnf  11601  ssnn0fi  12194  recan  13392  climconst  13600  dvdsext  14349  smupvallem  14450  smumullem  14459  pc11  14822  prmreclem4  14856  vdwmc2  14922  vdwlem8  14931  vdwlem13  14936  cshwsex  15064  cshws0  15065  prdsplusg  15349  prdsmulr  15350  prdsvsca  15351  prdshom  15358  imasplusg  15411  imasmulr  15412  imasip  15415  imasaddvallem  15428  imasvscaf  15438  quslem  15442  divsfval  15446  mrcuni  15520  catideu  15574  homfeqd  15593  comfeqd  15605  2oppccomf  15623  catcoppccl  15996  lublecllem  16227  pmtrrn  17091  pmtrfrn  17092  gsummptif1n0  17591  evlseu  18732  ip2eq  19213  frlmup4  19352  pmatcollpw2lem  19794  basdif0  19961  clsval2  20058  neif  20109  ordtbaslem  20197  ordtrest2lem  20212  lmconst  20270  cndis  20300  pnrmopn  20352  cmpfi  20416  finptfin  20526  comppfsc  20540  ptbasfi  20589  pttoponconst  20605  ptcnplem  20629  pthaus  20646  xkoptsub  20662  xkopt  20663  nrmr0reg  20757  ordthmeolem  20809  fbssfi  20845  filcon  20891  hausflim  20989  cnpflf  21009  fclscf  21033  cnpfcf  21049  alexsublem  21052  ptcmplem2  21061  ptcmplem3  21062  tsmsfbas  21135  eltsms  21140  utopbas  21243  isucn2  21287  psmetutop  21575  nrginvrcn  21687  lebnumlem3  21984  lebnumlem3OLD  21987  fmcfil  22235  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  mbfconst  22584  i1fmul  22647  itg2const  22691  itg2cnlem2  22713  itgle  22760  ibladdlem  22770  iblabs  22779  iblabsr  22780  iblmulc2  22781  bddmulibl  22789  ellimc2  22825  limcnlp  22826  c1lip1  22942  ply1nzb  23064  ulm0  23339  itgulm2  23357  dchrhash  24192  lgsquadlem2  24276  2sqlem10  24295  dchrisum  24323  rpvmasum2  24343  pntlemj  24434  axcontlem12  24998  uvtxnb  25218  usg2wlkeq2  25430  numclwwlkdisj  25801  rngoueqz  26151  ip2eqi  26491  ubthlem1  26505  hial2eq  26752  occon  26933  spanss  26994  pjnmopi  27794  ssmd1  27957  chrelat2i  28011  xrofsup  28346  ordtrest2NEWlem  28721  truae  29059  mbfmcst  29074  mbfmcnt  29083  dya2iocuni  29098  0rrv  29277  cvmliftlem15  30014  trpredss  30463  neibastop2lem  31009  tailf  31024  filnetlem4  31030  fin2so  31925  poimirlem26  31959  poimirlem28  31961  ismblfin  31974  cnambfre  31982  itg2addnclem  31986  itg2addnc  31989  itg2gt0cn  31990  ibladdnclem  31991  iblabsnc  31999  iblmulc2nc  32000  bddiblnc  32005  ftc1anclem6  32015  ftc1anclem7  32016  ftc1anclem8  32017  ftc1anc  32018  frinfm  32055  sdclem1  32065  ssbnd  32113  lssatle  32575  ltrneq2  33707  tendoeq2  34335  hbtlem7  35978  itgoss  36023  itgpowd  36093  trclrelexplem  36297  sumeq2ad  37638  prodeq2ad  37666  itgperiod  37852  stoweidlem35  37890  stoweidlem59  37914  fourierdlem31  37994  fourierdlem31OLD  37995  iundjiun  38292  hoiprodcl2  38371  ovnsslelem  38376  ovn0lem  38381  hoidmvlelem3  38413  2reurex  38596  opabn1stprc  39001  nbgr0edg  39408  rusgr1vtx  39586  rmsupp0  40140  lincop  40188  lcoc0  40202
  Copyright terms: Public domain W3C validator