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

Theorem ralrimivva 2878
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
ralrimivva.1
Assertion
Ref Expression
ralrimivva
Distinct variable groups:   , ,   ,

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3
21ex 434 . 2
32ralrimivv 2877 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807
This theorem is referenced by:  disjxiun  4449  otsndisj  4757  otiunsndisj  4758  swopo  4815  issod  4835  fcof1  6190  fliftfund  6211  soisores  6223  soisoi  6224  isocnv  6226  f1oiso  6247  oveqrspc2v  6319  caovclg  6467  caovcomg  6470  off  6554  caofrss  6573  caonncan  6578  dmmpt2g  6873  fnmpt2ovd  6878  fmpt2co  6883  poxp  6912  fvmpt2curryd  7019  smo11  7054  smoiso2  7059  omsmo  7322  qsdisj2  7408  eroprf  7428  dom2lem  7575  omxpenlem  7638  xpf1o  7699  unxpdomlem3  7746  fofinf1o  7821  dffi3  7911  supmo  7932  inf3lem6  8071  cantnf  8133  cantnfOLD  8155  rankxplim  8318  fseqenlem1  8426  fodomacn  8458  iunfictbso  8516  cofsmo  8670  infpssrlem5  8708  enfin2i  8722  fin23lem23  8727  fin23lem27  8729  fin23lem28  8741  compssiso  8775  ltordlem  10103  cju  10557  axdc4uzlem  12092  seqcaopr2  12143  seqhomo  12154  wrd2ind  12703  climcn2  13415  addcn2  13416  mulcn2  13418  o1of2  13435  isercolllem1  13487  fsum2dlem  13585  fsumcom2  13589  fprodser  13756  fprod2dlem  13784  fprodcom2  13788  isprm6  14250  crt  14308  eulerthlem2  14312  vdwlem12  14510  cshwsdisj  14583  imasaddfnlem  14925  imasvscafn  14934  mreexexd  15045  iscatd  15070  oppccomfpropd  15122  sectmon  15172  ssctr  15194  ssceq  15195  catsubcat  15208  issubc3  15218  fullsubc  15219  fullresc  15220  isfuncd  15234  idfucl  15250  cofucl  15257  funcres2b  15266  fulloppc  15291  fthoppc  15292  idffth  15302  cofull  15303  cofth  15304  ressffth  15307  setcmon  15414  setcepi  15415  resssetc  15419  resscatc  15432  catciso  15434  evlfcl  15491  uncfcurf  15508  hofcl  15528  yonedalem3  15549  yonedainv  15550  yonffthlem  15551  yoniso  15554  isdrs2  15568  isposd  15585  pospropd  15764  poslubmo  15776  posglbmo  15777  mgmplusf  15881  opifismgm  15885  ismndd  15943  mndpropd  15946  issubmnd  15948  mhmpropd  15972  idmhm  15975  mhmf1o  15976  issubmd  15980  0mhm  15989  resmhm  15990  resmhm2  15991  resmhm2b  15992  mhmco  15993  submacs  15996  prdspjmhm  15998  pwsdiagmhm  16000  pwsco1mhm  16001  pwsco2mhm  16002  gsumwspan  16014  frmdsssubm  16029  frmdup1  16032  grpsubf  16117  mhmmnd  16192  mhmfmhm  16193  issubg4  16220  grpissubg  16221  isnsg3  16235  nsgacs  16237  0nsg  16246  nsgid  16247  isghmd  16276  ghmmhm  16277  idghm  16282  ghmnsgima  16290  ghmnsgpreima  16291  ghmf1  16295  ghmf1o  16296  gaid  16337  subgga  16338  gass  16339  gasubg  16340  cntzsubm  16373  cntrsubgnsg  16378  lactghmga  16429  symgfixf1  16462  odf1  16584  sylow1lem2  16619  sylow2blem2  16641  sylow3lem1  16647  lsmssv  16663  lsmidm  16682  pj1eu  16714  efglem  16734  efgtf  16740  efgred  16766  efgredeu  16770  frgpmhm  16783  frgpuptf  16788  frgpuplem  16790  mulgmhm  16836  ghmcmn  16840  invghm  16842  ablnsg  16853  gsum2d2lem  17001  gsum2d2  17002  gsumcom2  17003  dprd2d2  17093  ablfaclem2  17137  srglmhm  17186  srgrmhm  17187  isrhm2d  17377  kerf1hrm  17392  issubrg2  17449  subrgint  17451  islmodd  17518  lmodscaf  17534  lmodprop2d  17572  islssd  17582  islss4  17608  lssacs  17613  lsspropd  17663  islmhmd  17685  lmhmima  17693  lmhmpreima  17694  reslmhm  17698  lspextmo  17702  lsmcl  17729  pj1lmhm  17746  islbs2  17800  issubrngd2  17835  opprdomn  17950  abvn0b  17951  issubassa2  17994  mvrf1  18081  mplsubglem  18093  mplsubglemOLD  18095  mplsubrg  18102  mplcoe5lem  18130  mplcoe2  18132  mplind  18167  evlslem2  18180  evlseu  18185  ply1sclf1  18330  expmhm  18485  nn0srg  18486  prmirredlem  18523  prmirredlemOLD  18526  expghm  18529  expghmOLD  18530  mulgghm2  18531  mulgghm2OLD  18534  domnchr  18569  znf1o  18590  zntoslem  18595  znfld  18599  cygznlem3  18608  phlipf  18687  dsmmlss  18775  uvcf1  18823  frlmlbs  18831  lindff1  18855  lindfrn  18856  f1lindf  18857  mamucl  18903  mamuass  18904  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  matbas2d  18925  mamumat1cl  18941  mamulid  18943  mamurid  18944  mat1mhm  18986  dmatid  18997  dmatsubcl  19000  dmatsgrp  19001  dmatmulcl  19002  dmatsrng  19003  dmatcrng  19004  scmatscmiddistr  19010  scmatscm  19015  scmatsgrp  19021  scmatsrng  19022  scmatcrng  19023  scmatsgrp1  19024  scmatsrng1  19025  scmatf1  19033  scmatmhm  19036  mavmul0g  19055  mdet1  19103  mdetunilem9  19122  mdetuni0  19123  mdetmul  19125  madutpos  19144  smadiadetlem4  19171  1elcpmat  19216  cpmatacl  19217  cpmatmcl  19220  mat2pmatf1  19230  mat2pmatmul  19232  mat2pmat1  19233  mat2pmatlin  19236  m2cpm  19242  m2cpminvid  19254  m2cpminvid2  19256  decpmatmul  19273  pmatcollpw1  19277  monmatcollpw  19280  pmatcollpw  19282  pmatcollpw3lem  19284  pmatcollpwscmatlem2  19291  pm2mpf1  19300  mp2pm2mplem4  19310  pm2mpmhmlem2  19320  chp0mat  19347  chpidmat  19348  tgclb  19472  mretopd  19593  toponmre  19594  iscldtop  19596  ordtbaslem  19689  ordtbas2  19692  cnt0  19847  haust1  19853  cnhaus  19855  isreg2  19878  dishaus  19883  ordthaus  19885  dfcon2  19920  iuncon  19929  clscon  19931  2ndcomap  19959  dis2ndc  19961  llynlly  19978  restnlly  19983  restlly  19984  islly2  19985  llyidm  19989  nllyidm  19990  hausllycmp  19995  kgentopon  20039  txbas  20068  ptbasin2  20079  ptbasfi  20082  txcnp  20121  txcnmpt  20125  pthaus  20139  tx1stc  20151  xkococnlem  20160  xkococn  20161  cnmpt21  20172  qtoptop2  20200  qtopeu  20217  kqt0lem  20237  isr0  20238  regr1lem2  20241  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  nrmr0reg  20250  reghmph  20294  nrmhmph  20295  txswaphmeo  20306  qtophmeo  20318  fbun  20341  trfbas2  20344  isfil2  20357  infil  20364  trfil2  20388  filssufilg  20412  hausflim  20482  fclsnei  20520  fclsfnflim  20528  flimfnfcls  20529  ptcmplem1  20552  clssubg  20607  tgpconcomp  20611  qustgplem  20619  tsmsfbas  20626  utoptop  20737  iducn  20786  cstucnd  20787  isxmetd  20829  isxmet2d  20830  xmettpos  20852  prdsdsf  20870  prdsmet  20873  ressprdsds  20874  imasdsf1olem  20876  imasf1oxmet  20878  imasf1omet  20879  blfvalps  20886  xmetresbl  20940  metss2  21015  comet  21016  stdbdmet  21019  stdbdmopn  21021  methaus  21023  met2ndci  21025  metustfbasOLD  21068  metustfbas  21069  nrmmetd  21095  subgngp  21149  ngptgp  21150  sranlm  21193  nlmvscnlem1  21195  nlmvscn  21196  nrginvrcn  21200  lssnlm  21209  nghmcn  21252  qtopbaslem  21265  reconn  21333  xmetdcn2  21342  metdscn  21360  metnrm  21366  elcncf1di  21399  cncffvrn  21402  mulc1cncf  21409  cncfco  21411  reparphti  21497  tchcph  21680  ipcnlem1  21685  ipcn  21686  iscfil3  21712  bcthlem5  21767  rrxmet  21835  minveclem3  21844  minveclem7  21850  ovolicc2lem4  21931  dyadmbl  22009  volcn  22015  itg1addlem1  22099  itg1addlem2  22104  itg1addlem4  22106  mbfi1fseqlem1  22122  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  dvmptfsum  22376  c1liplem1  22397  dvgt0lem2  22404  ftc1a  22438  ply1domn  22524  ply1divmo  22536  fta1b  22570  ig1peu  22572  coeeu  22622  plydivalg  22695  aaliou2b  22737  ulmss  22792  ulmcn  22794  efif1olem4  22932  efsubm  22938  logccv  23044  cvxcl  23314  basellem4  23357  fsumdvdscom  23461  musum  23467  dvdsmulf1o  23470  fsumdvdsmul  23471  dchrelbasd  23514  dchrmulcl  23524  dchrinv  23536  lgsqrlem2  23617  lgsdchr  23623  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  dchrisumlema  23673  dchrisumlem2  23675  chpdifbndlem2  23739  pntpbnd  23773  pntibndlem3  23777  axtgcont  23866  ercgrg  23908  idmot  23924  motco  23927  cnvmot  23928  motcgrg  23931  tgisline  24007  tghilbert1_2  24018  mirreu3  24035  mirmot  24055  ragperp  24094  foot  24096  mideu  24112  midf  24142  lmimot  24163  f1otrgds  24172  f1otrg  24174  f1otrge  24175  xmstrkgc  24189  brbtwn2  24208  axlowdimlem15  24259  axcontlem2  24268  axcontlem10  24276  eengtrkg  24288  eengtrkge  24289  usgraedgreu  24388  usgraidx2v  24393  wlknwwlkninj  24711  wlkiswwlkinj  24718  wwlkextinj  24730  clwwlkf1  24796  clwlkf1clwwlk  24850  2spotiundisj  25062  2spotmdisj  25068  numclwlk1lem2f1  25094  isgrp2d  25237  grpoinvf  25242  subgoablo  25313  ghgrplem2OLD  25369  ghabloOLD  25371  nvmf  25541  vacn  25604  nmcvcn  25605  smcnlem  25607  sspg  25641  ssps  25643  sspmlem  25645  0lno  25705  blocni  25720  sspph  25770  ipblnfi  25771  minvecolem7  25799  unopf1o  26835  cnvunop  26837  unoplin  26839  counop  26840  hmopadj2  26860  hmoplin  26861  bralnfn  26867  lnopeq0i  26926  hmops  26939  hmopm  26940  hmopco  26942  lnconi  26952  cnlnadjlem2  26987  adjmul  27011  adjadd  27012  cdjreui  27351  disjxpin  27447  off2  27481  f1od2  27547  xrofsup  27582  odutos  27651  abliso  27686  archiabllem1  27737  archiabllem2  27741  suborng  27805  xrge0slmod  27834  pstmxmet  27876  ofcf  28102  sibfof  28282  erdszelem4  28638  erdszelem9  28643  erdsze2lem2  28648  cnpcon  28675  pconcon  28676  txpcon  28677  ptpcon  28678  cvxpcon  28687  cvxscon  28688  iccllyscon  28695  cvmseu  28721  cvmliftmo  28729  cvmlift2lem5  28752  cvmlift2lem9  28756  mrsubff1  28874  elmrsubrn  28880  mrsubco  28881  msubff1  28916  mvhf1  28919  segconeu  29661  onsuct0  29906  fin2so  30040  heicant  30049  mblfinlem2  30052  ftc1anc  30098  fnessref  30175  neibastop1  30177  filnetlem3  30198  sdclem1  30236  isbnd3  30280  prdsbnd  30289  ismtycnv  30298  ismtyhmeolem  30300  ismtyres  30304  bfplem1  30318  bfplem2  30319  bfp  30320  rrnmet  30325  ismrer1  30334  iccbnd  30336  grpokerinj  30347  isdrngo2  30361  rngogrphom  30374  rngohomco  30377  rngoisocnv  30384  iscringd  30396  erprt  30614  nacsfix  30644  rmxypairf1o  30847  wepwsolem  30987  dnnumch3  30993  fnwe2  30999  mpaaeu  31099  idomsubgmo  31155  mon1psubm  31166  deg1mhm  31167  sumnnodd  31636  lptioo2  31637  lptioo1  31638  cncfshift  31676  cncfperiod  31681  dvnprodlem1  31743  fourierdlem42  31931  otiunsndisjX  32301  usgvincvadeu  32405  usgvincvadeuALT  32408  usgedgvadf1  32415  usgedgvadf1ALT  32418  ismgmd  32464  mgmhmpropd  32473  mgmhmf1o  32475  idmgmhm  32476  issubmgm2  32478  rabsubmgmd  32479  resmgmhm  32486  resmgmhm2  32487  resmgmhm2b  32488  mgmhmco  32489  submgmacs  32492  opmpt2ismgm  32495  mgmplusgiopALT  32518  isofn  32567  fthestrcsetc  32656  fullestrcsetc  32657  embedsetcestrclem  32663  fthsetcestrc  32671  fullsetcestrc  32672  isrnghm2d  32707  c0mgm  32715  c0mhm  32716  lidlmmgm  32731  2zlidl  32740  rnghmsscmap2  32781  rnghmsscmap  32782  rnghmsubcsetclem2  32784  rhmsscmap2  32827  rhmsscmap  32828  rhmsubcsetclem2  32830  rhmsscrnghm  32834  rhmsubcrngclem2  32836  srhmsubc  32884  fldhmsubc  32892  rhmsubc  32898  srhmsubcOLD  32903  fldhmsubcOLD  32911  rhmsubcOLD  32917  lindslinindsimp1  33058  lfl0f  34794  lkrlss  34820  lshpsmreu  34834  linepsubN  35476  pmapsub  35492  lautcnv  35814  lautco  35821  idltrn  35874  cdleme50f1  36269  cdleme50laut  36273  istendod  36488  dihf11  36994  dih1dimatlem  37056  lcfl7N  37228  lcfrlem9  37277  mapd1o  37375  hdmapf1oN  37595  hgmapf1oN  37633
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-ral 2812
  Copyright terms: Public domain W3C validator