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

Theorem ralrimivw 2735
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 2733 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   A.wral 2651
This theorem is referenced by:  2rmorex  3083  riinrab  4109  exse  4489  dmxp  5030  exse2  5180  mpt2eq12  6075  xpexgALT  6238  offveqb  6267  mpt2exg  6364  uniqs  6902  boxriin  7042  fisupg  7293  supmaxlem  7404  fisup2g  7406  fisupcl  7407  ordtypelem8  7429  r1val1  7647  scottex  7744  dfac12k  7962  compssiso  8189  axcclem  8272  ondomon  8373  tskuni  8593  pinq  8739  supexpr  8866  supmullem2  9909  zsupss  10499  qextlt  10723  qextle  10724  xrsupsslem  10819  xrinfmsslem  10820  supxrpnf  10831  recan  12069  climconst  12266  dvdsext  12829  smupvallem  12924  smumullem  12933  pc11  13182  prmreclem4  13216  vdwmc2  13276  vdwlem8  13285  vdwlem13  13290  prdsplusg  13610  prdsmulr  13611  prdsvsca  13612  prdshom  13618  imasplusg  13672  imasmulr  13673  imasaddvallem  13683  imasvscaf  13693  divslem  13697  divsfval  13701  mrcuni  13775  catideu  13829  homfeqd  13850  comfeqd  13862  2oppccomf  13880  catcoppccl  14192  lubid  14368  ip2eq  16809  basdif0  16943  clsval2  17039  neif  17089  ordtbaslem  17176  ordtrest2lem  17191  lmconst  17249  cndis  17279  pnrmopn  17331  cmpfi  17395  ptbasfi  17536  pttoponconst  17552  ptcnplem  17576  pthaus  17593  xkoptsub  17609  xkopt  17610  nrmr0reg  17704  ordthmeolem  17756  fbssfi  17792  filcon  17838  hausflim  17936  cnpflf  17956  fclscf  17980  cnpfcf  17996  alexsublem  17998  ptcmplem2  18007  ptcmplem3  18008  tsmsfbas  18080  eltsms  18085  utopbas  18188  isucn2  18232  metutop  18489  nrginvrcn  18600  lebnumlem3  18861  fmcfil  19098  ovolicc2lem4  19285  mbfconst  19396  i1fmul  19457  itg2const  19501  itg2cnlem2  19523  itgle  19570  ibladdlem  19580  iblabs  19589  iblabsr  19590  iblmulc2  19591  bddmulibl  19599  ellimc2  19633  limcnlp  19634  c1lip1  19750  evlseu  19806  ply1nzb  19914  ulm0  20176  itgulm2  20194  dchrhash  20924  lgsquadlem2  21008  2sqlem10  21027  dchrisum  21055  rpvmasum2  21075  pntlemj  21166  rngoueqz  21868  ip2eqi  22208  ubthlem1  22222  hial2eq  22458  occon  22639  spanss  22700  pjnmopi  23501  ssmd1  23664  chrelat2i  23718  xrofsup  23964  truae  24390  mbfmcst  24405  mbfmcnt  24414  dya2iocuni  24429  0rrv  24490  cvmliftlem15  24766  dedekind  24968  trpredss  25258  axcontlem12  25630  supadd  25950  itg2gt0cn  25962  ibladdnclem  25963  iblabsnc  25971  iblmulc2nc  25972  bddiblnc  25977  finptfin  26070  comppfsc  26080  neibastop2lem  26082  tailf  26097  filnetlem4  26103  frinfm  26130  sdclem1  26140  ssbnd  26190  frlmup4  26924  hbtlem7  27000  itgoss  27039  pmtrrn  27070  pmtrfrn  27071  stoweidlem35  27454  stoweidlem59  27478  2reurex  27629  lssatle  29132  ltrneq2  30264  tendoeq2  30890
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 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2656
  Copyright terms: Public domain W3C validator