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

Theorem ralrimivw 2856
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 2853 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   A.wral 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-ral 2796
This theorem is referenced by:  2rmorex  3288  riinrab  4387  exse  4829  dmxp  5207  mpt2eq12  6338  ovmpt3rabdm  6516  offveqb  6543  exse2  6720  xpexgALT  6774  mpt2exg  6856  uniqs  7369  boxriin  7509  fisupg  7766  supmaxlem  7922  fisup2g  7924  fisupcl  7925  ordtypelem8  7948  wemapso2  7977  cantnflem1  8106  r1val1  8202  scottex  8301  dfac12k  8525  compssiso  8752  axcclem  8835  ondomon  8936  tskuni  9159  pinq  9303  supexpr  9430  dedekind  9742  supmullem2  10511  zsupss  11175  qextlt  11406  qextle  11407  xrsupsslem  11502  xrinfmsslem  11503  supxrpnf  11514  ssnn0fi  12068  recan  13143  climconst  13340  dvdsext  13909  smupvallem  14005  smumullem  14014  pc11  14275  prmreclem4  14309  vdwmc2  14369  vdwlem8  14378  vdwlem13  14383  cshwsex  14457  cshws0  14458  prdsplusg  14727  prdsmulr  14728  prdsvsca  14729  prdshom  14736  imasplusg  14786  imasmulr  14787  imasip  14790  imasaddvallem  14798  imasvscaf  14808  quslem  14812  divsfval  14816  mrcuni  14890  catideu  14944  homfeqd  14962  comfeqd  14974  2oppccomf  14992  catcoppccl  15304  lublecllem  15487  pmtrrn  16351  pmtrfrn  16352  gsummptif1n0  16862  evlseu  18053  ip2eq  18555  frlmup4  18702  pmatcollpw2lem  19145  basdif0  19321  clsval2  19417  neif  19467  ordtbaslem  19555  ordtrest2lem  19570  lmconst  19628  cndis  19658  pnrmopn  19710  cmpfi  19774  finptfin  19885  comppfsc  19899  ptbasfi  19948  pttoponconst  19964  ptcnplem  19988  pthaus  20005  xkoptsub  20021  xkopt  20022  nrmr0reg  20116  ordthmeolem  20168  fbssfi  20204  filcon  20250  hausflim  20348  cnpflf  20368  fclscf  20392  cnpfcf  20408  alexsublem  20410  ptcmplem2  20419  ptcmplem3  20420  tsmsfbas  20492  eltsms  20497  utopbas  20604  isucn2  20648  metutopOLD  20951  psmetutop  20952  nrginvrcn  21066  lebnumlem3  21329  fmcfil  21577  ovolicc2lem4  21797  mbfconst  21908  i1fmul  21969  itg2const  22013  itg2cnlem2  22035  itgle  22082  ibladdlem  22092  iblabs  22101  iblabsr  22102  iblmulc2  22103  bddmulibl  22111  ellimc2  22147  limcnlp  22148  c1lip1  22264  ply1nzb  22389  ulm0  22651  itgulm2  22669  dchrhash  23411  lgsquadlem2  23495  2sqlem10  23514  dchrisum  23542  rpvmasum2  23562  pntlemj  23653  axcontlem12  24143  uvtxnb  24362  usg2wlkeq2  24574  numclwwlkdisj  24945  rngoueqz  25297  ip2eqi  25637  ubthlem1  25651  hial2eq  25888  occon  26070  spanss  26131  pjnmopi  26932  ssmd1  27095  chrelat2i  27149  xrofsup  27447  ordtrest2NEWlem  27770  truae  28081  mbfmcst  28096  mbfmcnt  28105  dya2iocuni  28120  0rrv  28256  cvmliftlem15  28609  trpredss  29280  fin2so  30008  supadd  30010  ismblfin  30023  cnambfre  30031  itg2addnclem  30034  itg2addnc  30037  itg2gt0cn  30038  ibladdnclem  30039  iblabsnc  30047  iblmulc2nc  30048  bddiblnc  30053  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  neibastop2lem  30146  tailf  30161  filnetlem4  30167  frinfm  30194  sdclem1  30204  ssbnd  30252  hbtlem7  31042  itgoss  31081  itgpowd  31151  itgperiod  31666  stoweidlem35  31702  stoweidlem59  31726  fourierdlem31  31805  2reurex  32020  rmsupp0  32671  lincop  32719  lcoc0  32733  lssatle  34442  ltrneq2  35574  tendoeq2  36202
  Copyright terms: Public domain W3C validator