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

Theorem ralrimivw 2628
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 24 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2626 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   A.wral 2544
This theorem is referenced by:  2rmorex  2970  riinrab  3978  exse  4356  dmxp  4896  exse2  5046  mpt2eq12  5869  xpexgALT  6031  offveqb  6060  mpt2exg  6157  uniqs  6714  boxriin  6853  fisupg  7100  supmaxlem  7210  fisup2g  7212  fisupcl  7213  ordtypelem8  7235  r1val1  7453  scottex  7550  dfac12k  7768  compssiso  7995  axcclem  8078  ondomon  8180  tskuni  8400  pinq  8546  supexpr  8673  lbinfm  9702  supmullem2  9716  zsupss  10302  qextlt  10524  qextle  10525  xrsupsslem  10619  xrinfmsslem  10620  supxrpnf  10631  recan  11814  climconst  12011  dvdsext  12573  smupvallem  12668  smumullem  12677  pc11  12926  prmreclem4  12960  vdwmc2  13020  vdwlem8  13029  vdwlem13  13034  prdsplusg  13352  prdsmulr  13353  prdsvsca  13354  prdshom  13360  imasplusg  13414  imasmulr  13415  imasaddvallem  13425  imasvscaf  13435  divslem  13439  divsfval  13443  mrcuni  13517  catideu  13571  homfeqd  13592  comfeqd  13604  2oppccomf  13622  catcoppccl  13934  lubid  14110  dprdval  15232  ip2eq  16551  basdif0  16685  clsval2  16781  neif  16831  ordtbaslem  16912  ordtrest2lem  16927  lmconst  16985  cndis  17013  pnrmopn  17065  cmpfi  17129  elpt  17261  elptr  17262  ptbasfi  17270  pttoponconst  17286  dfac14  17306  ptcnplem  17309  pthaus  17326  xkoptsub  17342  xkopt  17343  nrmr0reg  17434  ordthmeolem  17486  fbssfi  17526  filcon  17572  hausflim  17670  cnpflf  17690  fclscf  17714  cnpfcf  17730  alexsublem  17732  ptcmplem2  17741  ptcmplem3  17742  tsmsfbas  17804  eltsms  17809  nrginvrcn  18196  lebnumlem3  18455  fmcfil  18692  ovolicc2lem4  18873  mbfconst  18984  i1fmul  19045  itg2const  19089  itg2cnlem2  19111  itgle  19158  ibladdlem  19168  iblabs  19177  iblabsr  19178  iblmulc2  19179  bddmulibl  19187  ellimc2  19221  limcnlp  19222  c1lip1  19338  evlseu  19394  ply1nzb  19502  ulm0  19764  itgulm2  19779  dchrhash  20504  lgsquadlem2  20588  2sqlem10  20607  dchrisum  20635  rpvmasum2  20655  pntlemj  20746  rngoueqz  21089  ip2eqi  21427  ubthlem1  21441  hial2eq  21677  occon  21858  spanss  21919  pjnmopi  22720  ssmd1  22883  chrelat2i  22937  cvmliftlem15  23233  dedekind  23485  trpredss  23633  axcontlem12  24010  eqfnung2  24517  mapmapmap  24547  istopx  24946  finptfin  25696  comppfsc  25706  neibastop2lem  25708  tailf  25723  filnetlem4  25729  frinfm  25815  sdclem1  25852  ssbnd  25911  frlmup4  26652  hbtlem7  26728  itgoss  26767  pmtrrn  26798  pmtrfrn  26799  2reurex  27338  lssatle  28472  ltrneq2  29604  tendoeq2  30230
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-nf 1533  df-ral 2549
  Copyright terms: Public domain W3C validator