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

Theorem ralrimivva 3000
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 449 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 2999 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946
This theorem is referenced by:  disjord  4673  disjxiun  4681  disjxiunOLD  4682  otsndisj  5008  otiunsndisj  5009  swopo  5074  issod  5094  fcof1  6582  fliftfund  6603  isof1oidb  6614  isof1oopb  6615  soisores  6617  soisoi  6618  isocnv  6620  f1oiso  6641  oveqrspc2v  6713  oprres  6844  caovclg  6868  caovcomg  6871  off  6954  caofrss  6972  caonncan  6977  dmmpt2g  7288  fnmpt2ovd  7297  fmpt2co  7305  poxp  7334  fvmpt2curryd  7442  smo11  7506  smoiso2  7511  omsmo  7779  qsdisj2  7868  eroprf  7888  dom2lem  8037  omxpenlem  8102  xpf1o  8163  unxpdomlem3  8207  fofinf1o  8282  dffi3  8378  supmo  8399  infmo  8442  inf3lem6  8568  cantnf  8628  rankxplim  8780  fseqenlem1  8885  fodomacn  8917  iunfictbso  8975  cofsmo  9129  infpssrlem5  9167  enfin2i  9181  fin23lem23  9186  fin23lem27  9188  fin23lem28  9200  compssiso  9234  ltordlem  10591  cju  11054  axdc4uzlem  12822  seqcaopr2  12877  seqhomo  12888  wrd2ind  13523  cshf1  13602  s3sndisj  13752  s3iunsndisj  13753  climcn2  14367  addcn2  14368  mulcn2  14370  o1of2  14387  isercolllem1  14439  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fprodser  14723  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  isprm6  15473  crth  15530  eulerthlem2  15534  vdwlem12  15743  cshwsdisj  15852  imasaddfnlem  16235  imasvscafn  16244  mreexexd  16355  mreexexdOLD  16356  iscatd  16381  oppccomfpropd  16434  isofn  16482  sectmon  16489  ssctr  16532  ssceq  16533  catsubcat  16546  issubc3  16556  fullsubc  16557  fullresc  16558  isfuncd  16572  idfucl  16588  cofucl  16595  funcres2b  16604  fulloppc  16629  fthoppc  16630  idffth  16640  cofull  16641  cofth  16642  ressffth  16645  setcmon  16784  setcepi  16785  resssetc  16789  resscatc  16802  catciso  16804  fthestrcsetc  16837  fullestrcsetc  16838  embedsetcestrclem  16844  fthsetcestrc  16852  fullsetcestrc  16853  evlfcl  16909  uncfcurf  16926  hofcl  16946  yonedalem3  16967  yonedainv  16968  yonffthlem  16969  yoniso  16972  isdrs2  16986  isposd  17002  pospropd  17181  poslubmo  17193  posglbmo  17194  mgmplusf  17298  issstrmgm  17299  opifismgm  17305  ismndd  17360  mndpropd  17363  issubmnd  17365  mhmpropd  17388  idmhm  17391  mhmf1o  17392  issubmd  17396  0mhm  17405  resmhm  17406  resmhm2  17407  resmhm2b  17408  mhmco  17409  submacs  17412  prdspjmhm  17414  pwsdiagmhm  17416  pwsco1mhm  17417  pwsco2mhm  17418  gsumwspan  17430  frmdsssubm  17445  frmdup1  17448  grpsubf  17541  dfgrp3  17561  mhmmnd  17584  mhmfmhm  17585  issubg4  17660  grpissubg  17661  isnsg3  17675  nsgacs  17677  0nsg  17686  nsgid  17687  isghmd  17716  ghmmhm  17717  idghm  17722  ghmnsgima  17731  ghmnsgpreima  17732  ghmf1  17736  ghmf1o  17737  gaid  17778  subgga  17779  gass  17780  gasubg  17781  cntzsubm  17814  cntrsubgnsg  17819  lactghmga  17870  symgfixf1  17903  odf1  18025  sylow1lem2  18060  sylow2blem2  18082  sylow3lem1  18088  lsmssv  18104  lsmidm  18123  pj1eu  18155  efglem  18175  efgtf  18181  efgred  18207  efgredeu  18211  frgpmhm  18224  frgpuptf  18229  frgpuplem  18231  mulgmhm  18279  ghmcmn  18283  invghm  18285  ablnsg  18296  gsum2d2lem  18418  gsum2d2  18419  gsumcom2  18420  dprd2d2  18489  ablfaclem2  18531  srgfcl  18561  srglmhm  18581  srgrmhm  18582  isrhm2d  18776  kerf1hrm  18791  issubrg2  18848  subrgint  18850  islmodd  18917  lmodscaf  18933  lmodprop2d  18973  islssd  18984  islss4  19010  lssacs  19015  lsspropd  19065  islmhmd  19087  lmhmima  19095  lmhmpreima  19096  reslmhm  19100  lspextmo  19104  lsmcl  19131  pj1lmhm  19148  islbs2  19202  issubrngd2  19237  opprdomn  19349  abvn0b  19350  issubassa2  19393  mvrf1  19473  mplsubglem  19482  mplsubrg  19488  mplcoe5lem  19515  mplcoe2  19517  mplind  19550  evlslem2  19560  evlseu  19564  ply1sclf1  19707  expmhm  19863  nn0srg  19864  prmirredlem  19889  expghm  19892  mulgghm2  19893  domnchr  19928  znf1o  19948  zntoslem  19953  znfld  19957  cygznlem3  19966  phlipf  20045  dsmmlss  20136  uvcf1  20179  frlmlbs  20184  lindff1  20207  lindfrn  20208  f1lindf  20209  mamucl  20255  mamuass  20256  mamudi  20257  mamudir  20258  mamuvs1  20259  mamuvs2  20260  matbas2d  20277  mamumat1cl  20293  mamulid  20295  mamurid  20296  mat1mhm  20338  dmatid  20349  dmatsubcl  20352  dmatsgrp  20353  dmatmulcl  20354  dmatsrng  20355  dmatcrng  20356  scmatscmiddistr  20362  scmatscm  20367  scmatsgrp  20373  scmatsrng  20374  scmatcrng  20375  scmatsgrp1  20376  scmatsrng1  20377  scmatf1  20385  scmatmhm  20388  mavmul0g  20407  mdet1  20455  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  madutpos  20496  smadiadetlem4  20523  1elcpmat  20568  cpmatacl  20569  cpmatmcl  20572  mat2pmatf1  20582  mat2pmatmul  20584  mat2pmat1  20585  mat2pmatlin  20588  m2cpm  20594  m2cpminvid  20606  m2cpminvid2  20608  decpmatmul  20625  pmatcollpw1  20629  monmatcollpw  20632  pmatcollpw  20634  pmatcollpw3lem  20636  pmatcollpwscmatlem2  20643  pm2mpf1  20652  mp2pm2mplem4  20662  pm2mpmhmlem2  20672  chp0mat  20699  chpidmat  20700  tgclb  20822  mretopd  20944  toponmre  20945  iscldtop  20947  ordtbaslem  21040  ordtbas2  21043  cnt0  21198  haust1  21204  cnhaus  21206  isreg2  21229  dishaus  21234  ordthaus  21236  dfconn2  21270  iunconn  21279  clsconn  21281  2ndcomap  21309  dis2ndc  21311  llynlly  21328  restnlly  21333  restlly  21334  islly2  21335  llyidm  21339  nllyidm  21340  hausllycmp  21345  kgentopon  21389  txbas  21418  ptbasin2  21429  ptbasfi  21432  txcnp  21471  txcnmpt  21475  pthaus  21489  tx1stc  21501  xkococnlem  21510  xkococn  21511  cnmpt21  21522  qtoptop2  21550  qtopeu  21567  kqt0lem  21587  isr0  21588  regr1lem2  21591  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  nrmr0reg  21600  reghmph  21644  nrmhmph  21645  txswaphmeo  21656  qtophmeo  21668  fbun  21691  trfbas2  21694  isfil2  21707  infil  21714  trfil2  21738  filssufilg  21762  hausflim  21832  fclsnei  21870  fclsfnflim  21878  flimfnfcls  21879  ptcmplem1  21903  clssubg  21959  tgpconncomp  21963  qustgplem  21971  tsmsfbas  21978  utoptop  22085  iducn  22134  cstucnd  22135  isxmetd  22178  isxmet2d  22179  xmettpos  22201  prdsdsf  22219  prdsmet  22222  ressprdsds  22223  imasdsf1olem  22225  imasf1oxmet  22227  imasf1omet  22228  blfvalps  22235  xmetresbl  22289  metss2  22364  comet  22365  stdbdmet  22368  stdbdmopn  22370  methaus  22372  met2ndci  22374  metustfbas  22409  nrmmetd  22426  subgngp  22486  ngptgp  22487  sranlm  22535  nlmvscnlem1  22537  nlmvscn  22538  nrginvrcn  22543  lssnlm  22552  nghmcn  22596  qtopbaslem  22609  reconn  22678  xmetdcn2  22687  metdscn  22706  metnrm  22712  elcncf1di  22745  cncffvrn  22748  mulc1cncf  22755  cncfco  22757  reparphti  22843  isncvsngpd  22996  tchcph  23082  ipcnlem1  23090  ipcn  23091  iscfil3  23117  bcthlem5  23171  rrxmet  23237  minveclem3  23246  minveclem7  23252  ovolicc2lem4  23334  dyadmbl  23414  volcn  23420  itg1addlem1  23504  itg1addlem2  23509  itg1addlem4  23511  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  dvmptfsum  23783  c1liplem1  23804  dvgt0lem2  23811  ftc1a  23845  ply1domn  23928  ply1divmo  23940  fta1b  23974  ig1peu  23976  coeeu  24026  plydivalg  24099  aaliou2b  24141  ulmss  24196  ulmcn  24198  efif1olem4  24336  efsubm  24342  logccv  24454  logbmpt  24571  logbfval  24573  cvxcl  24756  basellem4  24855  fsumdvdscom  24956  musum  24962  dvdsmulf1o  24965  fsumdvdsmul  24966  dchrelbasd  25009  dchrmulcl  25019  dchrinv  25031  lgsqrlem2  25117  lgsdchr  25125  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  dchrisumlema  25222  dchrisumlem2  25224  chpdifbndlem2  25288  pntpbnd  25322  pntibndlem3  25326  axtgcont  25413  iscgrglt  25454  ercgrg  25457  idmot  25477  motco  25480  cnvmot  25481  motcgrg  25484  tgisline  25567  tghilberti2  25578  mirreu3  25594  mirmot  25615  ragperp  25657  foot  25659  mideu  25675  midf  25713  lmimot  25735  trgcopyeu  25743  f1otrgds  25794  f1otrg  25796  f1otrge  25797  xmstrkgc  25811  brbtwn2  25830  axlowdimlem15  25881  axcontlem2  25890  axcontlem10  25898  eengtrkg  25910  eengtrkge  25911  numedglnl  26084  usgredgreu  26155  uspgredg2vtxeu  26157  uspgredg2v  26161  usgredg2v  26164  wlkpwwlkf1ouspgr  26833  wlknwwlksninj  26843  wlkwwlkinj  26850  wwlksnextinj  26862  clwwlkf1  27012  clwlksf1clwwlk  27056  frcond4  27250  frgrncvvdeqlem8  27286  frgrncvvdeq  27289  frgrwopreglem4  27295  numclwlk1lem2f1  27347  grpoinvf  27514  nvmf  27628  vacn  27677  nmcvcn  27678  smcnlem  27680  sspg  27711  ssps  27713  sspmlem  27715  0lno  27773  blocni  27788  sspph  27838  ipblnfi  27839  minvecolem7  27867  unopf1o  28903  cnvunop  28905  unoplin  28907  counop  28908  hmopadj2  28928  hmoplin  28929  bralnfn  28935  lnopeq0i  28994  hmops  29007  hmopm  29008  hmopco  29010  lnconi  29020  cnlnadjlem2  29055  adjmul  29079  adjadd  29080  cdjreui  29419  disjxpin  29527  off2  29571  f1od2  29627  xrofsup  29661  odutos  29791  abliso  29824  archiabllem1  29875  archiabllem2  29879  suborng  29943  xrge0slmod  29972  1smat1  29998  submateq  30003  madjusmdetlem3  30023  pstmxmet  30068  ofcf  30293  ldgenpisys  30357  rossros  30371  inelcarsg  30501  sibfof  30530  sitmf  30542  hgt750lemb  30862  erdszelem4  31302  erdszelem9  31307  erdsze2lem2  31312  cnpconn  31338  pconnconn  31339  txpconn  31340  ptpconn  31341  cvxpconn  31350  cvxsconn  31351  iccllysconn  31358  cvmseu  31384  cvmliftmo  31392  cvmlift2lem5  31415  cvmlift2lem9  31419  mrsubff1  31537  elmrsubrn  31543  mrsubco  31544  msubff1  31579  mvhf1  31582  sslttr  32039  segconeu  32243  fnessref  32477  neibastop1  32479  filnetlem3  32500  onsuct0  32565  unblimceq0lem  32622  unbdqndv2  32627  knoppndv  32650  uncf  33518  fin2so  33526  poimirlem4  33543  poimirlem13  33552  poimirlem14  33553  poimirlem26  33565  heicant  33574  mblfinlem2  33577  ftc1anc  33623  sdclem1  33669  isbnd3  33713  prdsbnd  33722  ismtycnv  33731  ismtyhmeolem  33733  ismtyres  33737  bfplem1  33751  bfplem2  33752  bfp  33753  rrnmet  33758  ismrer1  33767  iccbnd  33769  grpokerinj  33822  isdrngo2  33887  rngogrphom  33900  rngohomco  33903  rngoisocnv  33910  iscringd  33927  erprt  34477  lfl0f  34674  lkrlss  34700  lshpsmreu  34714  linepsubN  35356  pmapsub  35372  lautcnv  35694  lautco  35701  idltrn  35754  cdleme50f1  36148  cdleme50laut  36152  istendod  36367  dihf11  36873  dih1dimatlem  36935  lcfl7N  37107  lcfrlem9  37156  mapd1o  37254  hdmapf1oN  37474  hgmapf1oN  37512  nacsfix  37592  rmxypairf1o  37793  wepwsolem  37929  dnnumch3  37934  fnwe2  37940  mpaaeu  38037  idomsubgmo  38093  mon1psubm  38101  deg1mhm  38102  isotone1  38663  isotone2  38664  disjxp1  39552  disjf1  39683  wessf1ornlem  39685  projf1o  39700  sumnnodd  40180  lptioo2  40181  lptioo1  40182  cncfshift  40405  cncfperiod  40410  dvnprodlem1  40479  fourierdlem42  40684  nnfoctbdjlem  40990  isomennd  41066  smflimlem6  41305  otiunsndisjX  41621  iccpartgt  41688  icceuelpart  41697  sprsymrelfolem2  42068  sprsymrelf  42070  ismgmd  42101  mgmhmpropd  42110  mgmhmf1o  42112  idmgmhm  42113  issubmgm2  42115  rabsubmgmd  42116  resmgmhm  42123  resmgmhm2  42124  resmgmhm2b  42125  mgmhmco  42126  submgmacs  42129  opmpt2ismgm  42132  mgmplusgiopALT  42155  isrnghm2d  42226  c0mgm  42234  c0mhm  42235  lidlmmgm  42250  2zlidl  42259  rnghmsscmap2  42298  rnghmsscmap  42299  rnghmsubcsetclem2  42301  rhmsscmap2  42344  rhmsscmap  42345  rhmsubcsetclem2  42347  rhmsscrnghm  42351  rhmsubcrngclem2  42353  srhmsubc  42401  fldhmsubc  42409  rhmsubc  42415  srhmsubcALTV  42419  fldhmsubcALTV  42427  rhmsubcALTV  42433  lindslinindsimp1  42571
  Copyright terms: Public domain W3C validator