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

Theorem ralrimivw 2790
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 2788 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  2rmorex  3152  riinrab  4234  exse  4671  dmxp  5045  mpt2eq12  6135  offveqb  6331  exse2  6506  xpexgALT  6559  mpt2exg  6637  uniqs  7148  boxriin  7293  fisupg  7548  supmaxlem  7702  fisup2g  7704  fisupcl  7705  ordtypelem8  7727  wemapso2  7756  cantnflem1  7885  r1val1  7981  scottex  8080  dfac12k  8304  compssiso  8531  axcclem  8614  ondomon  8715  tskuni  8938  pinq  9084  supexpr  9211  dedekind  9521  supmullem2  10285  zsupss  10932  qextlt  11161  qextle  11162  xrsupsslem  11257  xrinfmsslem  11258  supxrpnf  11269  recan  12808  climconst  13005  dvdsext  13567  smupvallem  13662  smumullem  13671  pc11  13929  prmreclem4  13963  vdwmc2  14023  vdwlem8  14032  vdwlem13  14037  cshwsex  14110  cshws0  14111  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  prdshom  14388  imasplusg  14438  imasmulr  14439  imasip  14442  imasaddvallem  14450  imasvscaf  14460  divslem  14464  divsfval  14468  mrcuni  14542  catideu  14596  homfeqd  14617  comfeqd  14629  2oppccomf  14647  catcoppccl  14959  lublecllem  15141  pmtrrn  15943  pmtrfrn  15944  ip2eq  17924  frlmup4  18071  basdif0  18400  clsval2  18496  neif  18546  ordtbaslem  18634  ordtrest2lem  18649  lmconst  18707  cndis  18737  pnrmopn  18789  cmpfi  18853  ptbasfi  18996  pttoponconst  19012  ptcnplem  19036  pthaus  19053  xkoptsub  19069  xkopt  19070  nrmr0reg  19164  ordthmeolem  19216  fbssfi  19252  filcon  19298  hausflim  19396  cnpflf  19416  fclscf  19440  cnpfcf  19456  alexsublem  19458  ptcmplem2  19467  ptcmplem3  19468  tsmsfbas  19540  eltsms  19545  utopbas  19652  isucn2  19696  metutopOLD  19999  psmetutop  20000  nrginvrcn  20114  lebnumlem3  20377  fmcfil  20625  ovolicc2lem4  20845  mbfconst  20955  i1fmul  21016  itg2const  21060  itg2cnlem2  21082  itgle  21129  ibladdlem  21139  iblabs  21148  iblabsr  21149  iblmulc2  21150  bddmulibl  21158  ellimc2  21194  limcnlp  21195  c1lip1  21311  evlseu  21368  ply1nzb  21479  ulm0  21741  itgulm2  21759  dchrhash  22495  lgsquadlem2  22579  2sqlem10  22598  dchrisum  22626  rpvmasum2  22646  pntlemj  22737  tgtrisegint  22834  axcontlem12  23044  elntg  23053  rngoueqz  23740  ip2eqi  24080  ubthlem1  24094  hial2eq  24331  occon  24513  spanss  24574  pjnmopi  25375  ssmd1  25538  chrelat2i  25592  fcnvgreu  25815  xrofsup  25878  submarchi  26027  ordtrest2NEWlem  26206  truae  26513  mbfmcst  26528  mbfmcnt  26537  dya2iocuni  26552  sseqf  26623  0rrv  26682  signsvvfval  26827  cvmliftlem15  27035  trpredss  27540  fin2so  28260  supadd  28262  ismblfin  28276  cnambfre  28284  itg2addnclem  28287  itg2addnc  28290  itg2gt0cn  28291  ibladdnclem  28292  iblabsnc  28300  iblmulc2nc  28301  bddiblnc  28306  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  finptfin  28413  comppfsc  28423  neibastop2lem  28425  tailf  28440  filnetlem4  28446  frinfm  28473  sdclem1  28483  ssbnd  28531  hbtlem7  29326  itgoss  29365  itgpowd  29435  stoweidlem35  29676  stoweidlem59  29700  2reurex  29851  ovmpt3rabdm  30008  uvtxnb  30124  usg2wlkeq2  30187  numclwwlkdisj  30519  rmsupp0  30612  lincop  30651  lcoc0  30665  lssatle  32233  ltrneq2  33365  tendoeq2  33991
  Copyright terms: Public domain W3C validator