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

Theorem ralrimivva 3159
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:   𝜑,𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝜓)
21ex 399 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 3158 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ral 3101
This theorem is referenced by:  disjord  4833  disjxiun  4841  otsndisj  5174  otiunsndisj  5175  swopo  5242  issod  5262  fcof1  6766  fliftfund  6787  isof1oidb  6798  isof1oopb  6799  soisores  6801  soisoi  6802  isocnv  6804  f1oiso  6825  oveqrspc2v  6901  oprres  7032  caovclg  7056  caovcomg  7059  off  7142  caofrss  7160  caonncan  7165  dmmpt2g  7476  fnmpt2ovd  7485  fnmpt2ovdOLD  7486  fmpt2co  7494  poxp  7523  fvmpt2curryd  7632  smo11  7697  smoiso2  7702  omsmo  7971  qsdisj2  8060  eroprf  8081  dom2lem  8232  omxpenlem  8300  xpf1o  8361  unxpdomlem3  8405  fofinf1o  8480  dffi3  8576  supmo  8597  infmo  8640  inf3lem6  8777  cantnf  8837  rankxplim  8989  fseqenlem1  9130  fodomacn  9162  iunfictbso  9220  cofsmo  9376  infpssrlem5  9414  enfin2i  9428  fin23lem23  9433  fin23lem27  9435  fin23lem28  9447  compssiso  9481  ltordlem  10838  cju  11301  axdc4uzlem  13006  seqcaopr2  13060  seqhomo  13071  wrd2ind  13701  cshf1  13780  s3sndisj  13931  s3iunsndisj  13932  climcn2  14546  addcn2  14547  mulcn2  14549  o1of2  14566  isercolllem1  14618  fsum2dlem  14724  fsumcom2  14728  fprodser  14900  fprod2dlem  14931  fprodcom2  14935  isprm6  15643  crth  15700  eulerthlem2  15704  vdwlem12  15913  cshwsdisj  16017  imasaddfnlem  16393  imasvscafn  16402  mreexexd  16513  iscatd  16538  oppccomfpropd  16591  isofn  16639  sectmon  16646  ssctr  16689  ssceq  16690  catsubcat  16703  issubc3  16713  fullsubc  16714  fullresc  16715  isfuncd  16729  idfucl  16745  cofucl  16752  funcres2b  16761  fulloppc  16786  fthoppc  16787  idffth  16797  cofull  16798  cofth  16799  ressffth  16802  setcmon  16941  setcepi  16942  resssetc  16946  resscatc  16959  catciso  16961  fthestrcsetc  16995  fullestrcsetc  16996  embedsetcestrclem  17002  fthsetcestrc  17010  fullsetcestrc  17011  evlfcl  17067  uncfcurf  17084  hofcl  17104  yonedalem3  17125  yonedainv  17126  yonffthlem  17127  yoniso  17130  isdrs2  17144  isposd  17160  pospropd  17339  poslubmo  17351  posglbmo  17352  mgmplusf  17456  issstrmgm  17457  opifismgm  17463  ismndd  17518  mndpropd  17521  issubmnd  17523  mhmpropd  17546  idmhm  17549  mhmf1o  17550  issubmd  17554  0mhm  17563  resmhm  17564  resmhm2  17565  resmhm2b  17566  mhmco  17567  submacs  17570  prdspjmhm  17572  pwsdiagmhm  17574  pwsco1mhm  17575  pwsco2mhm  17576  gsumwspan  17588  frmdsssubm  17603  frmdup1  17606  grpsubf  17699  dfgrp3  17719  mhmmnd  17742  mhmfmhm  17743  issubg4  17815  grpissubg  17816  isnsg3  17830  nsgacs  17832  0nsg  17841  nsgid  17842  isghmd  17871  ghmmhm  17872  idghm  17877  ghmnsgima  17886  ghmnsgpreima  17887  ghmf1  17891  ghmf1o  17892  gaid  17933  subgga  17934  gass  17935  gasubg  17936  cntzsubm  17969  cntrsubgnsg  17974  lactghmga  18025  symgfixf1  18058  odf1  18180  sylow1lem2  18215  sylow2blem2  18237  sylow3lem1  18243  lsmssv  18259  lsmidm  18278  pj1eu  18310  efglem  18330  efgtf  18336  efgred  18362  efgredeu  18366  frgpmhm  18379  frgpuptf  18384  frgpuplem  18386  mulgmhm  18434  ghmcmn  18438  invghm  18440  ablnsg  18451  gsum2d2lem  18573  gsum2d2  18574  gsumcom2  18575  dprd2d2  18645  ablfaclem2  18687  srgfcl  18717  srglmhm  18737  srgrmhm  18738  isrhm2d  18932  kerf1hrm  18947  issubrg2  19004  subrgint  19006  islmodd  19073  lmodscaf  19089  lmodprop2d  19129  islssd  19140  islss4  19169  lssacs  19174  lsspropd  19224  islmhmd  19246  lmhmima  19254  lmhmpreima  19255  reslmhm  19259  lspextmo  19263  lsmcl  19290  pj1lmhm  19307  islbs2  19363  issubrngd2  19398  opprdomn  19510  abvn0b  19511  issubassa2  19554  mvrf1  19634  mplsubglem  19643  mplsubrg  19649  mplcoe5lem  19676  mplcoe2  19678  mplind  19710  evlslem2  19720  evlseu  19724  ply1sclf1  19867  expmhm  20023  nn0srg  20024  prmirredlem  20049  expghm  20052  mulgghm2  20053  domnchr  20088  znf1o  20107  zntoslem  20112  znfld  20116  cygznlem3  20125  phlipf  20207  dsmmlss  20298  uvcf1  20341  frlmlbs  20346  lindff1  20369  lindfrn  20370  f1lindf  20371  mamucl  20417  mamuass  20418  mamudi  20419  mamudir  20420  mamuvs1  20421  mamuvs2  20422  matbas2d  20439  mamumat1cl  20455  mamulid  20457  mamurid  20458  mat1mhm  20501  dmatid  20512  dmatsubcl  20515  dmatsgrp  20516  dmatmulcl  20517  dmatsrng  20518  dmatcrng  20519  scmatscmiddistr  20525  scmatscm  20530  scmatsgrp  20536  scmatsrng  20537  scmatcrng  20538  scmatsgrp1  20539  scmatsrng1  20540  scmatf1  20548  scmatmhm  20551  mavmul0g  20570  mdet1  20618  mdetunilem9  20637  mdetuni0  20638  mdetmul  20640  madutpos  20659  smadiadetlem4  20687  1elcpmat  20733  cpmatacl  20734  cpmatmcl  20737  mat2pmatf1  20747  mat2pmatmul  20749  mat2pmat1  20750  mat2pmatlin  20753  m2cpm  20759  m2cpminvid  20771  m2cpminvid2  20773  decpmatmul  20790  pmatcollpw1  20794  monmatcollpw  20797  pmatcollpw  20799  pmatcollpw3lem  20801  pmatcollpwscmatlem2  20808  pm2mpf1  20817  mp2pm2mplem4  20827  pm2mpmhmlem2  20837  chp0mat  20864  chpidmat  20865  tgclb  20988  mretopd  21110  toponmre  21111  iscldtop  21113  ordtbaslem  21206  ordtbas2  21209  cnt0  21364  haust1  21370  cnhaus  21372  isreg2  21395  dishaus  21400  ordthaus  21402  dfconn2  21436  iunconn  21445  clsconn  21447  2ndcomap  21475  dis2ndc  21477  llynlly  21494  restnlly  21499  restlly  21500  islly2  21501  llyidm  21505  nllyidm  21506  hausllycmp  21511  kgentopon  21555  txbas  21584  ptbasin2  21595  ptbasfi  21598  txcnp  21637  txcnmpt  21641  pthaus  21655  tx1stc  21667  xkococnlem  21676  xkococn  21677  cnmpt21  21688  qtoptop2  21716  qtopeu  21733  kqt0lem  21753  isr0  21754  regr1lem2  21757  kqreglem1  21758  kqreglem2  21759  kqnrmlem1  21760  kqnrmlem2  21761  nrmr0reg  21766  reghmph  21810  nrmhmph  21811  txswaphmeo  21822  qtophmeo  21834  fbun  21857  trfbas2  21860  isfil2  21873  infil  21880  trfil2  21904  filssufilg  21928  hausflim  21998  fclsnei  22036  fclsfnflim  22044  flimfnfcls  22045  ptcmplem1  22069  clssubg  22125  tgpconncomp  22129  qustgplem  22137  tsmsfbas  22144  utoptop  22251  iducn  22300  cstucnd  22301  isxmetd  22344  isxmet2d  22345  xmettpos  22367  prdsdsf  22385  prdsmet  22388  ressprdsds  22389  imasdsf1olem  22391  imasf1oxmet  22393  imasf1omet  22394  blfvalps  22401  xmetresbl  22455  metss2  22530  comet  22531  stdbdmet  22534  stdbdmopn  22536  methaus  22538  met2ndci  22540  metustfbas  22575  nrmmetd  22592  subgngp  22652  ngptgp  22653  sranlm  22701  nlmvscnlem1  22703  nlmvscn  22704  nrginvrcn  22709  lssnlm  22718  nghmcn  22762  qtopbaslem  22775  reconn  22844  xmetdcn2  22853  metdscn  22872  metnrm  22878  elcncf1di  22911  cncffvrn  22914  mulc1cncf  22921  cncfco  22923  reparphti  23009  isncvsngpd  23162  tchcph  23248  ipcnlem1  23256  ipcn  23257  iscfil3  23283  bcthlem5  23337  rrxmet  23403  minveclem3  23412  minveclem7  23418  ovolicc2lem4  23501  dyadmbl  23581  volcn  23587  itg1addlem1  23673  itg1addlem2  23678  itg1addlem4  23680  mbfi1fseqlem1  23696  mbfi1fseqlem3  23698  mbfi1fseqlem4  23699  mbfi1fseqlem5  23700  dvmptfsum  23952  c1liplem1  23973  dvgt0lem2  23980  ftc1a  24014  ply1domn  24097  ply1divmo  24109  fta1b  24143  ig1peu  24145  coeeu  24195  plydivalg  24268  aaliou2b  24310  ulmss  24365  ulmcn  24367  efif1olem4  24506  efsubm  24512  logccv  24623  logbmpt  24740  logbfval  24742  cvxcl  24925  basellem4  25024  fsumdvdscom  25125  musum  25131  dvdsmulf1o  25134  fsumdvdsmul  25135  dchrelbasd  25178  dchrmulcl  25188  dchrinv  25200  lgsqrlem2  25286  lgsdchr  25294  lgseisenlem2  25315  lgsquadlem1  25319  lgsquadlem2  25320  dchrisumlema  25391  dchrisumlem2  25393  chpdifbndlem2  25457  pntpbnd  25491  pntibndlem3  25495  axtgcont  25582  iscgrglt  25623  ercgrg  25626  idmot  25646  motco  25649  cnvmot  25650  motcgrg  25653  tgisline  25736  tghilberti2  25747  mirreu3  25763  mirmot  25784  ragperp  25826  foot  25828  mideu  25844  midf  25882  lmimot  25904  trgcopyeu  25912  f1otrgds  25963  f1otrg  25965  f1otrge  25966  xmstrkgc  25980  brbtwn2  25999  axlowdimlem15  26050  axcontlem2  26059  axcontlem10  26067  eengtrkg  26079  eengtrkge  26080  numedglnl  26254  usgredgreu  26325  uspgredg2vtxeu  26327  uspgredg2v  26331  usgredg2v  26334  wlkswwlksf1o  27006  wlknwwlksninjOLD  27016  wlkwwlkinjOLD  27024  wwlksnextinj  27036  clwlkclwwlkf1  27153  clwwlkf1  27198  clwlksf1clwwlkOLD  27243  frcond4  27445  frgrncvvdeqlem8  27481  frgrncvvdeq  27484  frgrwopreglem4  27490  numclwwlk1lem2f1  27536  grpoinvf  27715  nvmf  27828  vacn  27877  nmcvcn  27878  smcnlem  27880  sspg  27911  ssps  27913  sspmlem  27915  0lno  27973  blocni  27988  sspph  28038  ipblnfi  28039  minvecolem7  28067  unopf1o  29103  cnvunop  29105  unoplin  29107  counop  29108  hmopadj2  29128  hmoplin  29129  bralnfn  29135  lnopeq0i  29194  hmops  29207  hmopm  29208  hmopco  29210  lnconi  29220  cnlnadjlem2  29255  adjmul  29279  adjadd  29280  cdjreui  29619  disjxpin  29726  off2  29770  f1od2  29826  xrofsup  29860  odutos  29988  abliso  30021  archiabllem1  30072  archiabllem2  30076  suborng  30140  xrge0slmod  30169  1smat1  30195  submateq  30200  madjusmdetlem3  30220  pstmxmet  30265  ofcf  30490  ldgenpisys  30554  rossros  30568  inelcarsg  30698  sibfof  30727  sitmf  30739  hgt750lemb  31059  erdszelem4  31499  erdszelem9  31504  erdsze2lem2  31509  cnpconn  31535  pconnconn  31536  txpconn  31537  ptpconn  31538  cvxpconn  31547  cvxsconn  31548  iccllysconn  31555  cvmseu  31581  cvmliftmo  31589  cvmlift2lem5  31612  cvmlift2lem9  31616  mrsubff1  31734  elmrsubrn  31740  mrsubco  31741  msubff1  31776  mvhf1  31779  sslttr  32235  segconeu  32439  fnessref  32673  neibastop1  32675  filnetlem3  32696  onsuct0  32757  unblimceq0lem  32814  unbdqndv2  32819  knoppndv  32842  uncf  33701  fin2so  33709  poimirlem4  33726  poimirlem13  33735  poimirlem14  33736  poimirlem26  33748  heicant  33757  mblfinlem2  33760  ftc1anc  33805  sdclem1  33850  isbnd3  33894  prdsbnd  33903  ismtycnv  33912  ismtyhmeolem  33914  ismtyres  33918  bfplem1  33932  bfplem2  33933  bfp  33934  rrnmet  33939  ismrer1  33948  iccbnd  33950  grpokerinj  34003  isdrngo2  34068  rngogrphom  34081  rngohomco  34084  rngoisocnv  34091  iscringd  34108  erprt  34652  lfl0f  34849  lkrlss  34875  lshpsmreu  34889  linepsubN  35532  pmapsub  35548  lautcnv  35870  lautco  35877  idltrn  35930  cdleme50f1  36324  cdleme50laut  36328  istendod  36543  dihf11  37048  dih1dimatlem  37110  lcfl7N  37282  lcfrlem9  37331  mapd1o  37429  hdmapf1oN  37646  hgmapf1oN  37684  nacsfix  37777  rmxypairf1o  37977  wepwsolem  38113  dnnumch3  38118  fnwe2  38124  mpaaeu  38221  idomsubgmo  38277  mon1psubm  38285  deg1mhm  38286  isotone1  38846  isotone2  38847  disjxp1  39731  disjf1  39858  wessf1ornlem  39860  projf1o  39875  sumnnodd  40342  lptioo2  40343  lptioo1  40344  cncfshift  40567  cncfperiod  40572  dvnprodlem1  40641  fourierdlem42  40845  nnfoctbdjlem  41151  isomennd  41227  smflimlem6  41466  otiunsndisjX  41869  iccpartgt  41938  icceuelpart  41947  sprsymrelfolem2  42311  sprsymrelf  42313  ismgmd  42344  mgmhmpropd  42353  mgmhmf1o  42355  idmgmhm  42356  issubmgm2  42358  rabsubmgmd  42359  resmgmhm  42366  resmgmhm2  42367  resmgmhm2b  42368  mgmhmco  42369  submgmacs  42372  opmpt2ismgm  42375  mgmplusgiopALT  42398  isrnghm2d  42469  c0mgm  42477  c0mhm  42478  lidlmmgm  42493  2zlidl  42502  rnghmsscmap2  42541  rnghmsscmap  42542  rnghmsubcsetclem2  42544  rhmsscmap2  42587  rhmsscmap  42588  rhmsubcsetclem2  42590  rhmsscrnghm  42594  rhmsubcrngclem2  42596  srhmsubc  42644  fldhmsubc  42652  rhmsubc  42658  srhmsubcALTV  42662  fldhmsubcALTV  42670  rhmsubcALTV  42676  lindslinindsimp1  42814
  Copyright terms: Public domain W3C validator