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

Theorem ralrimivw 2821
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 25 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2819 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-ral 2741
This theorem is referenced by:  2rmorex  3184  riinrab  4267  exse  4705  dmxp  5079  mpt2eq12  6167  offveqb  6363  exse2  6538  xpexgALT  6591  mpt2exg  6669  uniqs  7181  boxriin  7326  fisupg  7581  supmaxlem  7735  fisup2g  7737  fisupcl  7738  ordtypelem8  7760  wemapso2  7789  cantnflem1  7918  r1val1  8014  scottex  8113  dfac12k  8337  compssiso  8564  axcclem  8647  ondomon  8748  tskuni  8971  pinq  9117  supexpr  9244  dedekind  9554  supmullem2  10318  zsupss  10965  qextlt  11194  qextle  11195  xrsupsslem  11290  xrinfmsslem  11291  supxrpnf  11302  recan  12845  climconst  13042  dvdsext  13605  smupvallem  13700  smumullem  13709  pc11  13967  prmreclem4  14001  vdwmc2  14061  vdwlem8  14070  vdwlem13  14075  cshwsex  14148  cshws0  14149  prdsplusg  14417  prdsmulr  14418  prdsvsca  14419  prdshom  14426  imasplusg  14476  imasmulr  14477  imasip  14480  imasaddvallem  14488  imasvscaf  14498  divslem  14502  divsfval  14506  mrcuni  14580  catideu  14634  homfeqd  14655  comfeqd  14667  2oppccomf  14685  catcoppccl  14997  lublecllem  15179  pmtrrn  15984  pmtrfrn  15985  gsummptif1n0  16479  evlseu  17624  ip2eq  18104  frlmup4  18251  basdif0  18580  clsval2  18676  neif  18726  ordtbaslem  18814  ordtrest2lem  18829  lmconst  18887  cndis  18917  pnrmopn  18969  cmpfi  19033  ptbasfi  19176  pttoponconst  19192  ptcnplem  19216  pthaus  19233  xkoptsub  19249  xkopt  19250  nrmr0reg  19344  ordthmeolem  19396  fbssfi  19432  filcon  19478  hausflim  19576  cnpflf  19596  fclscf  19620  cnpfcf  19636  alexsublem  19638  ptcmplem2  19647  ptcmplem3  19648  tsmsfbas  19720  eltsms  19725  utopbas  19832  isucn2  19876  metutopOLD  20179  psmetutop  20180  nrginvrcn  20294  lebnumlem3  20557  fmcfil  20805  ovolicc2lem4  21025  mbfconst  21135  i1fmul  21196  itg2const  21240  itg2cnlem2  21262  itgle  21309  ibladdlem  21319  iblabs  21328  iblabsr  21329  iblmulc2  21330  bddmulibl  21338  ellimc2  21374  limcnlp  21375  c1lip1  21491  ply1nzb  21616  ulm0  21878  itgulm2  21896  dchrhash  22632  lgsquadlem2  22716  2sqlem10  22735  dchrisum  22763  rpvmasum2  22783  pntlemj  22874  tgtrisegint  22974  axcontlem12  23243  elntg  23252  rngoueqz  23939  ip2eqi  24279  ubthlem1  24293  hial2eq  24530  occon  24712  spanss  24773  pjnmopi  25574  ssmd1  25737  chrelat2i  25791  fcnvgreu  26013  xrofsup  26077  submarchi  26225  ordtrest2NEWlem  26374  truae  26681  mbfmcst  26696  mbfmcnt  26705  dya2iocuni  26720  sseqf  26797  0rrv  26856  signsvvfval  27001  cvmliftlem15  27209  trpredss  27715  fin2so  28442  supadd  28444  ismblfin  28458  cnambfre  28466  itg2addnclem  28469  itg2addnc  28472  itg2gt0cn  28473  ibladdnclem  28474  iblabsnc  28482  iblmulc2nc  28483  bddiblnc  28488  ftc1anclem6  28498  ftc1anclem7  28499  ftc1anclem8  28500  ftc1anc  28501  finptfin  28595  comppfsc  28605  neibastop2lem  28607  tailf  28622  filnetlem4  28628  frinfm  28655  sdclem1  28665  ssbnd  28713  hbtlem7  29507  itgoss  29546  itgpowd  29616  stoweidlem35  29856  stoweidlem59  29880  2reurex  30031  ovmpt3rabdm  30188  uvtxnb  30304  usg2wlkeq2  30367  numclwwlkdisj  30699  ssnn0fi  30775  rmsupp0  30811  scmatid  30921  lincop  30939  lcoc0  30953  pmatcollpw2lem  31120  lssatle  32756  ltrneq2  33888  tendoeq2  34514
  Copyright terms: Public domain W3C validator