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

Theorem ralrimiv 2869
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.)
Hypothesis
Ref Expression
ralrimiv.1
Assertion
Ref Expression
ralrimiv
Distinct variable group:   ,

Proof of Theorem ralrimiv
StepHypRef Expression
1 ax-5 1704 . 2
2 ralrimiv.1 . 2
31, 2hbralrimi 2853 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralrimiva  2871  ralrimivw  2872  ralrimdv  2873  ralrimivv  2877  reximdvai  2929  r19.27v  2990  rr19.3v  3241  rabssdv  3579  rzal  3931  trin  4555  class2seteq  4620  ralxfrALT  4671  otiunsndisj  4758  onmindif  4972  issref  5385  fnprb  6129  fnprOLD  6130  ssorduni  6621  onminex  6642  onmindif2  6647  suceloni  6648  limuni3  6687  frxp  6910  poxp  6912  onfununi  7031  onnseq  7034  tfrlem12  7077  tz7.48-2  7126  oaass  7229  omass  7248  oelim2  7263  oelimcl  7268  oaabs2  7313  omabs  7315  undifixp  7525  dom2lem  7575  isinf  7753  unblem4  7795  unbnn2  7797  marypha1lem  7913  supiso  7954  ordiso2  7961  card2inf  8002  elirrv  8044  wemapwe  8160  wemapweOLD  8161  trcl  8180  tz9.13  8230  rankval3b  8265  rankunb  8289  rankuni2b  8292  scott0  8325  dfac8alem  8431  carduniima  8498  alephsmo  8504  alephval3  8512  iunfictbso  8516  dfac3  8523  dfac5lem5  8529  dfac12r  8547  dfac12k  8548  kmlem4  8554  kmlem11  8561  cfsuc  8658  cofsmo  8670  cfsmolem  8671  coftr  8674  alephsing  8677  infpssrlem3  8706  fin23lem30  8743  isf32lem2  8755  isf32lem3  8756  isf34lem6  8781  fin1a2lem11  8811  fin1a2lem13  8813  fin1a2s  8815  axcc2lem  8837  domtriomlem  8843  axdc3lem2  8852  axdc4lem  8856  axcclem  8858  axdclem2  8921  iundom2g  8936  uniimadom  8940  cardmin  8960  alephval2  8968  alephreg  8978  fpwwe2lem12  9040  wunex2  9137  wuncval2  9146  tskwe2  9172  inar1  9174  tskuni  9182  gruun  9205  intgru  9213  grutsk1  9220  genpcl  9407  ltexprlem5  9439  suplem1pr  9451  supexpr  9453  supsrlem  9509  axpre-sup  9567  supmul1  10533  supmullem1  10534  supmul  10536  peano5nni  10564  uzind  10979  zindd  10990  uzwo  11173  uzwoOLD  11174  lbzbi  11199  xrsupsslem  11527  xrinfmsslem  11528  supxrun  11536  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  icoshftf1o  11672  flval3  11951  axdc4uzlem  12092  ccatrn  12606  2cshw  12781  cshweqrep  12789  sqrlem1  13076  sqrlem6  13081  fsum0diag2  13598  alzdvds  14036  gcdcllem1  14149  maxprmfct  14254  unbenlem  14426  vdwlem6  14504  vdwlem10  14508  firest  14830  mrieqv2d  15036  iscatd  15070  setcmon  15414  setcepi  15415  isglbd  15747  isacs4lem  15798  acsfiindd  15807  acsmapd  15808  psss  15844  ghmrn  16280  ghmpreima  16288  cntz2ss  16370  symgextres  16450  psgnunilem2  16520  lsmsubg  16674  efgsfo  16757  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsummptnn0fzfv  17016  dmdprdd  17030  dprd2da  17091  imasring  17268  isabvd  17469  issrngd  17510  islssd  17582  lbsextlem3  17806  lbsextlem4  17807  lidldvgen  17903  psgnghm  18616  isphld  18689  frlmsslsp  18829  frlmsslspOLD  18830  mp2pm2mplem4  19310  tgcl  19471  distop  19497  indistopon  19502  pptbas  19509  toponmre  19594  opnnei  19621  neiuni  19623  neindisj2  19624  ordtrest2  19705  cnpnei  19765  cnindis  19793  cmpcld  19902  uncmp  19903  hauscmplem  19906  2ndc1stc  19952  1stcrest  19954  1stcelcls  19962  llyrest  19986  nllyrest  19987  cldllycmp  19996  reftr  20015  locfincf  20032  comppfsc  20033  txcls  20105  ptpjcn  20112  ptclsg  20116  dfac14lem  20118  xkoccn  20120  txlly  20137  txnlly  20138  ptrescn  20140  tx1stc  20151  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  qtopeu  20217  hmeofval  20259  ordthmeolem  20302  isfild  20359  fbasrn  20385  trfil2  20388  flimclslem  20485  fclsrest  20525  fclscf  20526  flimfcls  20527  alexsubALTlem1  20547  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALT  20551  qustgpopn  20618  isxmetd  20829  imasdsf1olem  20876  blcls  21009  prdsxmslem2  21032  metustfbasOLD  21068  metustfbas  21069  dscmet  21093  nrmmetd  21095  reperflem  21323  reconnlem2  21332  xrge0tsms  21339  fsumcn  21374  cnheibor  21455  tchcph  21680  lmmbr  21697  caubl  21746  ivthlem1  21863  ovolctb  21901  ovoliunlem2  21914  ovolscalem1  21924  ovolicc2  21933  voliunlem3  21962  ismbfd  22047  mbfimaopnlem  22062  itg2le  22146  ellimc2  22281  c1liplem1  22397  plyeq0lem  22607  dgreq0  22662  aannenlem1  22724  pilem2  22847  cxpcn3lem  23121  scvxcvx  23315  musum  23467  dchrisum0flb  23695  ostth2lem2  23819  usgrares1  24410  nbusgra  24428  nbgra0nb  24429  nbgra0edg  24432  cusgrafilem2  24480  usgrasscusgra  24483  uvtxnbgravtx  24495  fargshiftf  24636  fargshiftfva  24639  usg2wlkeq  24708  clwwlkn0  24774  clwwisshclwwlem  24806  0egra0rgra  24936  eupatrl  24968  eupap1  24976  3cyclfrgrarn  25013  vdgn1frgrav3  25028  2spotiundisj  25062  numclwlk2lem2f1o  25105  frgraregord013  25118  htthlem  25834  ocsh  26201  shintcli  26247  pjss2coi  27083  pjnormssi  27087  pjclem4  27118  pj3si  27126  pj3cor1i  27128  strlem3a  27171  strb  27177  hstrlem3a  27179  hstrbi  27185  spansncv2  27212  mdsl1i  27240  cvmdi  27243  mdexchi  27254  h1da  27268  mdsymlem6  27327  sumdmdii  27334  dmdbr5ati  27341  isoun  27520  supssd  27527  xrge0tsmsd  27775  ordtrest2NEW  27905  pwsiga  28130  measiun  28189  dya2iocuni  28254  erdszelem8  28642  cvmsss2  28719  cvmfolem  28724  rtrclreclem.min  29070  dfrtrcl2  29071  dfon2lem8  29222  dfon2lem9  29223  dfon2  29224  rdgprc  29227  trpredtr  29313  trpredmintr  29314  trpredelss  29315  dftrpred3g  29316  trpredpo  29318  trpredrec  29321  wfrlem15  29357  frr3g  29386  frrlem5b  29392  frrlem5d  29394  sltval2  29416  supaddc  30041  supadd  30042  heicant  30049  mblfinlem1  30051  ftc2nc  30099  nn0prpwlem  30140  ntruni  30145  clsint2  30147  fneint  30166  fnessref  30175  refssfne  30176  neibastop1  30177  neibastop2lem  30178  sdclem2  30235  fdc  30238  seqpo  30240  prdsbnd  30289  heibor  30317  rrnequiv  30331  0idl  30422  intidl  30426  unichnidl  30428  prnc  30464  pellfundre  30817  pellfundge  30818  pellfundlb  30820  dford3lem1  30968  aomclem2  31001  hashgcdeq  31158  addrcom  31384  dvmptfprod  31742  dvnprodlem3  31745  funressnfv  32213  tz6.12-afv  32258  otiunsndisjX  32301  nnsgrp  32505  fullestrcsetc  32657  fullsetcestrc  32672  ellcoellss  33036  lindsrng01  33069  iunconlem2  33735  bnj518  33944  bnj1137  34051  bnj1136  34053  bnj1413  34091  bnj1417  34097  bnj60  34118  lsmcv2  34754  lcvexchlem4  34762  lcvexchlem5  34763  eqlkr  34824  paddclN  35566  pclfinN  35624  ldilcnv  35839  ldilco  35840  cdleme25dN  36082  cdlemj2  36548  tendocan  36550  erng1lem  36713  erngdvlem4-rN  36725  dihord2pre  36952  dihglblem2N  37021  dochvalr  37084  hdmap14lem12  37609  hdmap14lem13  37610  pwinfi3  37748
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-ral 2812
  Copyright terms: Public domain W3C validator