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

Theorem ralrimivw 2758
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 23 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2756 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   A.wral 2674
This theorem is referenced by:  2rmorex  3106  riinrab  4134  exse  4514  dmxp  5055  exse2  5205  mpt2eq12  6101  xpexgALT  6264  offveqb  6293  mpt2exg  6390  uniqs  6931  boxriin  7071  fisupg  7322  supmaxlem  7433  fisup2g  7435  fisupcl  7436  ordtypelem8  7458  r1val1  7676  scottex  7773  dfac12k  7991  compssiso  8218  axcclem  8301  ondomon  8402  tskuni  8622  pinq  8768  supexpr  8895  supmullem2  9939  zsupss  10529  qextlt  10753  qextle  10754  xrsupsslem  10849  xrinfmsslem  10850  supxrpnf  10861  recan  12103  climconst  12300  dvdsext  12863  smupvallem  12958  smumullem  12967  pc11  13216  prmreclem4  13250  vdwmc2  13310  vdwlem8  13319  vdwlem13  13324  prdsplusg  13644  prdsmulr  13645  prdsvsca  13646  prdshom  13652  imasplusg  13706  imasmulr  13707  imasaddvallem  13717  imasvscaf  13727  divslem  13731  divsfval  13735  mrcuni  13809  catideu  13863  homfeqd  13884  comfeqd  13896  2oppccomf  13914  catcoppccl  14226  lubid  14402  ip2eq  16847  basdif0  16981  clsval2  17077  neif  17127  ordtbaslem  17214  ordtrest2lem  17229  lmconst  17287  cndis  17317  pnrmopn  17369  cmpfi  17433  ptbasfi  17574  pttoponconst  17590  ptcnplem  17614  pthaus  17631  xkoptsub  17647  xkopt  17648  nrmr0reg  17742  ordthmeolem  17794  fbssfi  17830  filcon  17876  hausflim  17974  cnpflf  17994  fclscf  18018  cnpfcf  18034  alexsublem  18036  ptcmplem2  18045  ptcmplem3  18046  tsmsfbas  18118  eltsms  18123  utopbas  18226  isucn2  18270  metutopOLD  18573  psmetutop  18574  nrginvrcn  18688  lebnumlem3  18949  fmcfil  19186  ovolicc2lem4  19377  mbfconst  19488  i1fmul  19549  itg2const  19593  itg2cnlem2  19615  itgle  19662  ibladdlem  19672  iblabs  19681  iblabsr  19682  iblmulc2  19683  bddmulibl  19691  ellimc2  19725  limcnlp  19726  c1lip1  19842  evlseu  19898  ply1nzb  20006  ulm0  20268  itgulm2  20286  dchrhash  21016  lgsquadlem2  21100  2sqlem10  21119  dchrisum  21147  rpvmasum2  21167  pntlemj  21258  rngoueqz  21979  ip2eqi  22319  ubthlem1  22333  hial2eq  22569  occon  22750  spanss  22811  pjnmopi  23612  ssmd1  23775  chrelat2i  23829  xrofsup  24087  truae  24555  mbfmcst  24570  mbfmcnt  24579  dya2iocuni  24594  0rrv  24670  cvmliftlem15  24946  dedekind  25148  trpredss  25454  axcontlem12  25826  supadd  26146  ismblfin  26154  cnambfre  26162  itg2addnclem  26163  itg2addnc  26166  itg2gt0cn  26167  ibladdnclem  26168  iblabsnc  26176  iblmulc2nc  26177  bddiblnc  26182  finptfin  26275  comppfsc  26285  neibastop2lem  26287  tailf  26302  filnetlem4  26308  frinfm  26335  sdclem1  26345  ssbnd  26395  frlmup4  27129  hbtlem7  27205  itgoss  27244  pmtrrn  27275  pmtrfrn  27276  stoweidlem35  27659  stoweidlem59  27683  2reurex  27834  lssatle  29510  ltrneq2  30642  tendoeq2  31268
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2679
  Copyright terms: Public domain W3C validator