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

Theorem ralrimivva 2954
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 2953 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901
This theorem is referenced by:  disjxiun  4574  disjxiunOLD  4575  otsndisj  4895  otiunsndisj  4896  swopo  4959  issod  4979  fcof1  6420  fliftfund  6441  isof1oidb  6452  isof1oopb  6453  soisores  6455  soisoi  6456  isocnv  6458  f1oiso  6479  oveqrspc2v  6550  oprres  6678  caovclg  6702  caovcomg  6705  off  6788  caofrss  6806  caonncan  6811  dmmpt2g  7110  fnmpt2ovd  7117  fmpt2co  7125  poxp  7154  fvmpt2curryd  7262  smo11  7326  smoiso2  7331  omsmo  7599  qsdisj2  7690  eroprf  7710  dom2lem  7859  omxpenlem  7924  xpf1o  7985  unxpdomlem3  8029  fofinf1o  8104  dffi3  8198  supmo  8219  infmo  8262  inf3lem6  8391  cantnf  8451  rankxplim  8603  fseqenlem1  8708  fodomacn  8740  iunfictbso  8798  cofsmo  8952  infpssrlem5  8990  enfin2i  9004  fin23lem23  9009  fin23lem27  9011  fin23lem28  9023  compssiso  9057  ltordlem  10405  cju  10866  axdc4uzlem  12602  seqcaopr2  12657  seqhomo  12668  wrd2ind  13278  cshf1  13356  s3sndisj  13503  s3iunsndisj  13504  climcn2  14120  addcn2  14121  mulcn2  14123  o1of2  14140  isercolllem1  14192  fsum2dlem  14292  fsumcom2  14296  fsumcom2OLD  14297  fprodser  14467  fprod2dlem  14498  fprodcom2  14502  fprodcom2OLD  14503  isprm6  15213  crth  15270  eulerthlem2  15274  vdwlem12  15483  cshwsdisj  15592  imasaddfnlem  15960  imasvscafn  15969  mreexexd  16080  mreexexdOLD  16081  iscatd  16106  oppccomfpropd  16159  isofn  16207  sectmon  16214  ssctr  16257  ssceq  16258  catsubcat  16271  issubc3  16281  fullsubc  16282  fullresc  16283  isfuncd  16297  idfucl  16313  cofucl  16320  funcres2b  16329  fulloppc  16354  fthoppc  16355  idffth  16365  cofull  16366  cofth  16367  ressffth  16370  setcmon  16509  setcepi  16510  resssetc  16514  resscatc  16527  catciso  16529  fthestrcsetc  16562  fullestrcsetc  16563  embedsetcestrclem  16569  fthsetcestrc  16577  fullsetcestrc  16578  evlfcl  16634  uncfcurf  16651  hofcl  16671  yonedalem3  16692  yonedainv  16693  yonffthlem  16694  yoniso  16697  isdrs2  16711  isposd  16727  pospropd  16906  poslubmo  16918  posglbmo  16919  mgmplusf  17023  issstrmgm  17024  opifismgm  17030  ismndd  17085  mndpropd  17088  issubmnd  17090  mhmpropd  17113  idmhm  17116  mhmf1o  17117  issubmd  17121  0mhm  17130  resmhm  17131  resmhm2  17132  resmhm2b  17133  mhmco  17134  submacs  17137  prdspjmhm  17139  pwsdiagmhm  17141  pwsco1mhm  17142  pwsco2mhm  17143  gsumwspan  17155  frmdsssubm  17170  frmdup1  17173  grpsubf  17266  dfgrp3  17286  mhmmnd  17309  mhmfmhm  17310  issubg4  17385  grpissubg  17386  isnsg3  17400  nsgacs  17402  0nsg  17411  nsgid  17412  isghmd  17441  ghmmhm  17442  idghm  17447  ghmnsgima  17456  ghmnsgpreima  17457  ghmf1  17461  ghmf1o  17462  gaid  17504  subgga  17505  gass  17506  gasubg  17507  cntzsubm  17540  cntrsubgnsg  17545  lactghmga  17596  symgfixf1  17629  odf1  17751  sylow1lem2  17786  sylow2blem2  17808  sylow3lem1  17814  lsmssv  17830  lsmidm  17849  pj1eu  17881  efglem  17901  efgtf  17907  efgred  17933  efgredeu  17937  frgpmhm  17950  frgpuptf  17955  frgpuplem  17957  mulgmhm  18005  ghmcmn  18009  invghm  18011  ablnsg  18022  gsum2d2lem  18144  gsum2d2  18145  gsumcom2  18146  dprd2d2  18215  ablfaclem2  18257  srgfcl  18287  srglmhm  18307  srgrmhm  18308  isrhm2d  18500  kerf1hrm  18515  issubrg2  18572  subrgint  18574  islmodd  18641  lmodscaf  18657  lmodprop2d  18697  islssd  18706  islss4  18732  lssacs  18737  lsspropd  18787  islmhmd  18809  lmhmima  18817  lmhmpreima  18818  reslmhm  18822  lspextmo  18826  lsmcl  18853  pj1lmhm  18870  islbs2  18924  issubrngd2  18959  opprdomn  19071  abvn0b  19072  issubassa2  19115  mvrf1  19195  mplsubglem  19204  mplsubrg  19210  mplcoe5lem  19237  mplcoe2  19239  mplind  19272  evlslem2  19282  evlseu  19286  ply1sclf1  19429  expmhm  19583  nn0srg  19584  prmirredlem  19608  expghm  19611  mulgghm2  19612  domnchr  19647  znf1o  19667  zntoslem  19672  znfld  19676  cygznlem3  19685  phlipf  19764  dsmmlss  19855  uvcf1  19898  frlmlbs  19903  lindff1  19926  lindfrn  19927  f1lindf  19928  mamucl  19974  mamuass  19975  mamudi  19976  mamudir  19977  mamuvs1  19978  mamuvs2  19979  matbas2d  19996  mamumat1cl  20012  mamulid  20014  mamurid  20015  mat1mhm  20057  dmatid  20068  dmatsubcl  20071  dmatsgrp  20072  dmatmulcl  20073  dmatsrng  20074  dmatcrng  20075  scmatscmiddistr  20081  scmatscm  20086  scmatsgrp  20092  scmatsrng  20093  scmatcrng  20094  scmatsgrp1  20095  scmatsrng1  20096  scmatf1  20104  scmatmhm  20107  mavmul0g  20126  mdet1  20174  mdetunilem9  20193  mdetuni0  20194  mdetmul  20196  madutpos  20215  smadiadetlem4  20242  1elcpmat  20287  cpmatacl  20288  cpmatmcl  20291  mat2pmatf1  20301  mat2pmatmul  20303  mat2pmat1  20304  mat2pmatlin  20307  m2cpm  20313  m2cpminvid  20325  m2cpminvid2  20327  decpmatmul  20344  pmatcollpw1  20348  monmatcollpw  20351  pmatcollpw  20353  pmatcollpw3lem  20355  pmatcollpwscmatlem2  20362  pm2mpf1  20371  mp2pm2mplem4  20381  pm2mpmhmlem2  20391  chp0mat  20418  chpidmat  20419  tgclb  20533  mretopd  20654  toponmre  20655  iscldtop  20657  ordtbaslem  20750  ordtbas2  20753  cnt0  20908  haust1  20914  cnhaus  20916  isreg2  20939  dishaus  20944  ordthaus  20946  dfcon2  20980  iuncon  20989  clscon  20991  2ndcomap  21019  dis2ndc  21021  llynlly  21038  restnlly  21043  restlly  21044  islly2  21045  llyidm  21049  nllyidm  21050  hausllycmp  21055  kgentopon  21099  txbas  21128  ptbasin2  21139  ptbasfi  21142  txcnp  21181  txcnmpt  21185  pthaus  21199  tx1stc  21211  xkococnlem  21220  xkococn  21221  cnmpt21  21232  qtoptop2  21260  qtopeu  21277  kqt0lem  21297  isr0  21298  regr1lem2  21301  kqreglem1  21302  kqreglem2  21303  kqnrmlem1  21304  kqnrmlem2  21305  nrmr0reg  21310  reghmph  21354  nrmhmph  21355  txswaphmeo  21366  qtophmeo  21378  fbun  21402  trfbas2  21405  isfil2  21418  infil  21425  trfil2  21449  filssufilg  21473  hausflim  21543  fclsnei  21581  fclsfnflim  21589  flimfnfcls  21590  ptcmplem1  21614  clssubg  21670  tgpconcomp  21674  qustgplem  21682  tsmsfbas  21689  utoptop  21796  iducn  21845  cstucnd  21846  isxmetd  21889  isxmet2d  21890  xmettpos  21912  prdsdsf  21930  prdsmet  21933  ressprdsds  21934  imasdsf1olem  21936  imasf1oxmet  21938  imasf1omet  21939  blfvalps  21946  xmetresbl  22000  metss2  22075  comet  22076  stdbdmet  22079  stdbdmopn  22081  methaus  22083  met2ndci  22085  metustfbas  22120  nrmmetd  22137  subgngp  22197  ngptgp  22198  sranlm  22246  nlmvscnlem1  22248  nlmvscn  22249  nrginvrcn  22254  lssnlm  22263  nghmcn  22307  qtopbaslem  22320  reconn  22387  xmetdcn2  22396  metdscn  22415  metnrm  22421  elcncf1di  22454  cncffvrn  22457  mulc1cncf  22464  cncfco  22466  reparphti  22553  isncvsngpd  22703  tchcph  22789  ipcnlem1  22797  ipcn  22798  iscfil3  22824  bcthlem5  22878  rrxmet  22944  minveclem3  22953  minveclem7  22959  ovolicc2lem4  23040  dyadmbl  23119  volcn  23125  itg1addlem1  23210  itg1addlem2  23215  itg1addlem4  23217  mbfi1fseqlem1  23233  mbfi1fseqlem3  23235  mbfi1fseqlem4  23236  mbfi1fseqlem5  23237  dvmptfsum  23487  c1liplem1  23508  dvgt0lem2  23515  ftc1a  23549  ply1domn  23632  ply1divmo  23644  fta1b  23678  ig1peu  23680  coeeu  23730  plydivalg  23803  aaliou2b  23845  ulmss  23900  ulmcn  23902  efif1olem4  24040  efsubm  24046  logccv  24154  logbmpt  24271  logbfval  24273  cvxcl  24456  basellem4  24555  fsumdvdscom  24656  musum  24662  dvdsmulf1o  24665  fsumdvdsmul  24666  dchrelbasd  24709  dchrmulcl  24719  dchrinv  24731  lgsqrlem2  24817  lgsdchr  24825  lgseisenlem2  24846  lgsquadlem1  24850  lgsquadlem2  24851  dchrisumlema  24922  dchrisumlem2  24924  chpdifbndlem2  24988  pntpbnd  25022  pntibndlem3  25026  axtgcont  25113  iscgrglt  25155  ercgrg  25158  idmot  25178  motco  25181  cnvmot  25182  motcgrg  25185  tgisline  25268  tghilberti2  25279  mirreu3  25295  mirmot  25316  ragperp  25358  foot  25360  mideu  25376  midf  25414  lmimot  25436  trgcopyeu  25444  f1otrgds  25495  f1otrg  25497  f1otrge  25498  xmstrkgc  25512  brbtwn2  25531  axlowdimlem15  25582  axcontlem2  25591  axcontlem10  25599  eengtrkg  25611  eengtrkge  25612  usgraedgreu  25711  usgraidx2v  25716  wlknwwlkninj  26033  wlkiswwlkinj  26040  wwlkextinj  26052  clwwlkf1  26118  clwlkf1clwwlk  26171  2spotiundisj  26383  2spotmdisj  26389  numclwlk1lem2f1  26415  grpoinvf  26564  nvmf  26678  vacn  26727  nmcvcn  26728  smcnlem  26730  sspg  26761  ssps  26763  sspmlem  26765  0lno  26823  blocni  26838  sspph  26888  ipblnfi  26889  minvecolem7  26917  unopf1o  27953  cnvunop  27955  unoplin  27957  counop  27958  hmopadj2  27978  hmoplin  27979  bralnfn  27985  lnopeq0i  28044  hmops  28057  hmopm  28058  hmopco  28060  lnconi  28070  cnlnadjlem2  28105  adjmul  28129  adjadd  28130  cdjreui  28469  disjxpin  28577  off2  28617  f1od2  28681  xrofsup  28717  odutos  28788  abliso  28821  archiabllem1  28872  archiabllem2  28876  suborng  28940  xrge0slmod  28969  1smat1  28992  submateq  28997  madjusmdetlem3  29017  pstmxmet  29062  ofcf  29286  ldgenpisys  29350  rossros  29364  inelcarsg  29494  sibfof  29523  sitmf  29535  erdszelem4  30224  erdszelem9  30229  erdsze2lem2  30234  cnpcon  30260  pconcon  30261  txpcon  30262  ptpcon  30263  cvxpcon  30272  cvxscon  30273  iccllyscon  30280  cvmseu  30306  cvmliftmo  30314  cvmlift2lem5  30337  cvmlift2lem9  30341  mrsubff1  30459  elmrsubrn  30465  mrsubco  30466  msubff1  30501  mvhf1  30504  segconeu  31082  fnessref  31316  neibastop1  31318  filnetlem3  31339  onsuct0  31404  unblimceq0lem  31461  unbdqndv2  31466  knoppndv  31489  uncf  32352  fin2so  32360  poimirlem4  32377  poimirlem13  32386  poimirlem14  32387  poimirlem26  32399  heicant  32408  mblfinlem2  32411  ftc1anc  32457  sdclem1  32503  isbnd3  32547  prdsbnd  32556  ismtycnv  32565  ismtyhmeolem  32567  ismtyres  32571  bfplem1  32585  bfplem2  32586  bfp  32587  rrnmet  32592  ismrer1  32601  iccbnd  32603  grpokerinj  32656  isdrngo2  32721  rngogrphom  32734  rngohomco  32737  rngoisocnv  32744  iscringd  32761  erprt  32970  lfl0f  33168  lkrlss  33194  lshpsmreu  33208  linepsubN  33850  pmapsub  33866  lautcnv  34188  lautco  34195  idltrn  34248  cdleme50f1  34643  cdleme50laut  34647  istendod  34862  dihf11  35368  dih1dimatlem  35430  lcfl7N  35602  lcfrlem9  35651  mapd1o  35749  hdmapf1oN  35969  hgmapf1oN  36007  nacsfix  36087  rmxypairf1o  36288  wepwsolem  36424  dnnumch3  36429  fnwe2  36435  mpaaeu  36533  idomsubgmo  36589  mon1psubm  36597  deg1mhm  36598  isotone1  37160  isotone2  37161  disjxp1  38057  disjf1  38158  wessf1ornlem  38160  projf1o  38175  sumnnodd  38491  lptioo2  38492  lptioo1  38493  cncfshift  38553  cncfperiod  38558  dvnprodlem1  38630  fourierdlem42  38836  nnfoctbdjlem  39142  isomennd  39215  smflimlem6  39456  iccpartgt  39760  icceuelpart  39769  otiunsndisjX  40122  usgredgreu  40437  uspgredg2vtxeu  40439  uspgredg2v  40443  usgredg2v  40446  1wlkpwwlkf1ouspgr  41068  wlknwwlksninj  41078  wlkwwlkinj  41085  wwlksnextinj  41097  clwwlksf1  41216  clwlksf1clwwlk  41268  frgrncvvdeq  41472  av-numclwlk1lem2f1  41516  ismgmd  41558  mgmhmpropd  41567  mgmhmf1o  41569  idmgmhm  41570  issubmgm2  41572  rabsubmgmd  41573  resmgmhm  41580  resmgmhm2  41581  resmgmhm2b  41582  mgmhmco  41583  submgmacs  41586  opmpt2ismgm  41589  mgmplusgiopALT  41612  isrnghm2d  41683  c0mgm  41691  c0mhm  41692  lidlmmgm  41707  2zlidl  41716  rnghmsscmap2  41757  rnghmsscmap  41758  rnghmsubcsetclem2  41760  rhmsscmap2  41803  rhmsscmap  41804  rhmsubcsetclem2  41806  rhmsscrnghm  41810  rhmsubcrngclem2  41812  srhmsubc  41860  fldhmsubc  41868  rhmsubc  41874  srhmsubcALTV  41879  fldhmsubcALTV  41887  rhmsubcALTV  41893  lindslinindsimp1  42032
  Copyright terms: Public domain W3C validator