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

Theorem rexlimiv 2943
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
Hypothesis
Ref Expression
rexlimiv.1
Assertion
Ref Expression
rexlimiv
Distinct variable group:   ,

Proof of Theorem rexlimiv
StepHypRef Expression
1 rexlimiv.1 . . 3
21rgen 2817 . 2
3 r19.23v 2937 . 2
42, 3mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807  E.wrex 2808
This theorem is referenced by:  rexlimiva  2945  rexlimivw  2946  rexlimdv  2947  rexlimivv  2954  r19.36v  3005  r19.44v  3014  r19.45v  3015  rexn0  3932  uniss2  4282  disjiun  4442  elres  5314  ssimaex  5938  ordzsl  6680  onzsl  6681  tfrlem8  7072  nneob  7320  ecoptocl  7420  mapsn  7480  elixpsn  7528  ixpsnf1o  7529  php  7721  php3  7723  ssfi  7760  findcard  7779  findcard2  7780  ordunifi  7790  fiint  7817  en3lp  8054  inf0  8059  inf3lemd  8065  inf3lem6  8071  noinfep  8097  cantnfvalf  8105  trcl  8180  bndrank  8280  rankc2  8310  tcrank  8323  ficardom  8363  ac10ct  8436  isinfcard  8494  alephfp  8510  dfac5lem4  8528  dfac2  8532  ackbij2  8644  fin23lem16  8736  fin23lem29  8742  fin17  8795  fin1a2lem6  8806  itunitc  8822  hsmexlem9  8826  axdc3lem2  8852  axdc3lem4  8854  axcclem  8858  zorn2lem7  8903  wunr1om  9118  tskr1om  9166  grothomex  9228  prnmadd  9396  ltaprlem  9443  mulgt0sr  9503  0re  9617  0cnALT  9832  renegcli  9903  infmrcl  10547  peano2nn  10573  bndndx  10819  uzn0  11125  ublbneg  11195  om2uzrani  12063  uzrdgfni  12069  exprelprel  12528  rexanuz2  13182  caurcvg  13499  caucvg  13501  infcvgaux1i  13668  vdwlem6  14504  efgrelexlemb  16768  cygth  18610  iscldtop  19596  opnneiid  19627  pnfnei  19721  mnfnei  19722  discmp  19898  cmpsublem  19899  cmpfi  19908  bwthOLD  19911  2ndcredom  19951  2ndc1stc  19952  2ndcdisj  19957  kgenidm  20048  methaus  21023  xrtgioo  21311  caun0  21720  ovolmge0  21888  itg2lcl  22134  aannenlem2  22725  aannenlem3  22726  aaliou2  22736  leibpilem1  23271  2sqlem2  23639  ostth  23824  eupatrl  24968  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  zerdivemp1  25436  rngoridfz  25437  h1de2ctlem  26473  h1de2ci  26474  spansni  26475  spanunsni  26497  riesz3i  26981  adjbd1o  27004  rnbra  27026  pjnmopi  27067  dfpjop  27101  atom1d  27272  cvexchlem  27287  cdj1i  27352  cdj3lem1  27353  hasheuni  28091  cvmlift2lem12  28759  mrsubccat  28878  msrid  28905  elmthm  28936  ghomgrpilem2  29026  rtrclreclem.trans  29069  rtrclind  29072  untint  29084  dfon2lem3  29217  dfon2lem7  29221  dfrdg2  29228  trpred0  29319  nodmon  29410  sltval2  29416  bdayfo  29435  nofulllem5  29466  finminlem  30136  fneint  30166  zerdivemp1x  30358  ismrc  30633  eldiophb  30690  eldioph4b  30745  dfacbasgrp  31057  dochsnnz  37177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator