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  4579  disjxiunOLD  4580  otsndisj  4904  otiunsndisj  4905  swopo  4969  issod  4989  fcof1  6442  fliftfund  6463  isof1oidb  6474  isof1oopb  6475  soisores  6477  soisoi  6478  isocnv  6480  f1oiso  6501  oveqrspc2v  6572  oprres  6700  caovclg  6724  caovcomg  6727  off  6810  caofrss  6828  caonncan  6833  dmmpt2g  7132  fnmpt2ovd  7139  fmpt2co  7147  poxp  7176  fvmpt2curryd  7284  smo11  7348  smoiso2  7353  omsmo  7621  qsdisj2  7712  eroprf  7732  dom2lem  7881  omxpenlem  7946  xpf1o  8007  unxpdomlem3  8051  fofinf1o  8126  dffi3  8220  supmo  8241  infmo  8284  inf3lem6  8413  cantnf  8473  rankxplim  8625  fseqenlem1  8730  fodomacn  8762  iunfictbso  8820  cofsmo  8974  infpssrlem5  9012  enfin2i  9026  fin23lem23  9031  fin23lem27  9033  fin23lem28  9045  compssiso  9079  ltordlem  10432  cju  10893  axdc4uzlem  12644  seqcaopr2  12699  seqhomo  12710  wrd2ind  13329  cshf1  13407  s3sndisj  13554  s3iunsndisj  13555  climcn2  14171  addcn2  14172  mulcn2  14174  o1of2  14191  isercolllem1  14243  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fprodser  14518  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  isprm6  15264  crth  15321  eulerthlem2  15325  vdwlem12  15534  cshwsdisj  15643  imasaddfnlem  16011  imasvscafn  16020  mreexexd  16131  mreexexdOLD  16132  iscatd  16157  oppccomfpropd  16210  isofn  16258  sectmon  16265  ssctr  16308  ssceq  16309  catsubcat  16322  issubc3  16332  fullsubc  16333  fullresc  16334  isfuncd  16348  idfucl  16364  cofucl  16371  funcres2b  16380  fulloppc  16405  fthoppc  16406  idffth  16416  cofull  16417  cofth  16418  ressffth  16421  setcmon  16560  setcepi  16561  resssetc  16565  resscatc  16578  catciso  16580  fthestrcsetc  16613  fullestrcsetc  16614  embedsetcestrclem  16620  fthsetcestrc  16628  fullsetcestrc  16629  evlfcl  16685  uncfcurf  16702  hofcl  16722  yonedalem3  16743  yonedainv  16744  yonffthlem  16745  yoniso  16748  isdrs2  16762  isposd  16778  pospropd  16957  poslubmo  16969  posglbmo  16970  mgmplusf  17074  issstrmgm  17075  opifismgm  17081  ismndd  17136  mndpropd  17139  issubmnd  17141  mhmpropd  17164  idmhm  17167  mhmf1o  17168  issubmd  17172  0mhm  17181  resmhm  17182  resmhm2  17183  resmhm2b  17184  mhmco  17185  submacs  17188  prdspjmhm  17190  pwsdiagmhm  17192  pwsco1mhm  17193  pwsco2mhm  17194  gsumwspan  17206  frmdsssubm  17221  frmdup1  17224  grpsubf  17317  dfgrp3  17337  mhmmnd  17360  mhmfmhm  17361  issubg4  17436  grpissubg  17437  isnsg3  17451  nsgacs  17453  0nsg  17462  nsgid  17463  isghmd  17492  ghmmhm  17493  idghm  17498  ghmnsgima  17507  ghmnsgpreima  17508  ghmf1  17512  ghmf1o  17513  gaid  17555  subgga  17556  gass  17557  gasubg  17558  cntzsubm  17591  cntrsubgnsg  17596  lactghmga  17647  symgfixf1  17680  odf1  17802  sylow1lem2  17837  sylow2blem2  17859  sylow3lem1  17865  lsmssv  17881  lsmidm  17900  pj1eu  17932  efglem  17952  efgtf  17958  efgred  17984  efgredeu  17988  frgpmhm  18001  frgpuptf  18006  frgpuplem  18008  mulgmhm  18056  ghmcmn  18060  invghm  18062  ablnsg  18073  gsum2d2lem  18195  gsum2d2  18196  gsumcom2  18197  dprd2d2  18266  ablfaclem2  18308  srgfcl  18338  srglmhm  18358  srgrmhm  18359  isrhm2d  18551  kerf1hrm  18566  issubrg2  18623  subrgint  18625  islmodd  18692  lmodscaf  18708  lmodprop2d  18748  islssd  18757  islss4  18783  lssacs  18788  lsspropd  18838  islmhmd  18860  lmhmima  18868  lmhmpreima  18869  reslmhm  18873  lspextmo  18877  lsmcl  18904  pj1lmhm  18921  islbs2  18975  issubrngd2  19010  opprdomn  19122  abvn0b  19123  issubassa2  19166  mvrf1  19246  mplsubglem  19255  mplsubrg  19261  mplcoe5lem  19288  mplcoe2  19290  mplind  19323  evlslem2  19333  evlseu  19337  ply1sclf1  19480  expmhm  19634  nn0srg  19635  prmirredlem  19660  expghm  19663  mulgghm2  19664  domnchr  19699  znf1o  19719  zntoslem  19724  znfld  19728  cygznlem3  19737  phlipf  19816  dsmmlss  19907  uvcf1  19950  frlmlbs  19955  lindff1  19978  lindfrn  19979  f1lindf  19980  mamucl  20026  mamuass  20027  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  matbas2d  20048  mamumat1cl  20064  mamulid  20066  mamurid  20067  mat1mhm  20109  dmatid  20120  dmatsubcl  20123  dmatsgrp  20124  dmatmulcl  20125  dmatsrng  20126  dmatcrng  20127  scmatscmiddistr  20133  scmatscm  20138  scmatsgrp  20144  scmatsrng  20145  scmatcrng  20146  scmatsgrp1  20147  scmatsrng1  20148  scmatf1  20156  scmatmhm  20159  mavmul0g  20178  mdet1  20226  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  madutpos  20267  smadiadetlem4  20294  1elcpmat  20339  cpmatacl  20340  cpmatmcl  20343  mat2pmatf1  20353  mat2pmatmul  20355  mat2pmat1  20356  mat2pmatlin  20359  m2cpm  20365  m2cpminvid  20377  m2cpminvid2  20379  decpmatmul  20396  pmatcollpw1  20400  monmatcollpw  20403  pmatcollpw  20405  pmatcollpw3lem  20407  pmatcollpwscmatlem2  20414  pm2mpf1  20423  mp2pm2mplem4  20433  pm2mpmhmlem2  20443  chp0mat  20470  chpidmat  20471  tgclb  20585  mretopd  20706  toponmre  20707  iscldtop  20709  ordtbaslem  20802  ordtbas2  20805  cnt0  20960  haust1  20966  cnhaus  20968  isreg2  20991  dishaus  20996  ordthaus  20998  dfcon2  21032  iuncon  21041  clscon  21043  2ndcomap  21071  dis2ndc  21073  llynlly  21090  restnlly  21095  restlly  21096  islly2  21097  llyidm  21101  nllyidm  21102  hausllycmp  21107  kgentopon  21151  txbas  21180  ptbasin2  21191  ptbasfi  21194  txcnp  21233  txcnmpt  21237  pthaus  21251  tx1stc  21263  xkococnlem  21272  xkococn  21273  cnmpt21  21284  qtoptop2  21312  qtopeu  21329  kqt0lem  21349  isr0  21350  regr1lem2  21353  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  nrmr0reg  21362  reghmph  21406  nrmhmph  21407  txswaphmeo  21418  qtophmeo  21430  fbun  21454  trfbas2  21457  isfil2  21470  infil  21477  trfil2  21501  filssufilg  21525  hausflim  21595  fclsnei  21633  fclsfnflim  21641  flimfnfcls  21642  ptcmplem1  21666  clssubg  21722  tgpconcomp  21726  qustgplem  21734  tsmsfbas  21741  utoptop  21848  iducn  21897  cstucnd  21898  isxmetd  21941  isxmet2d  21942  xmettpos  21964  prdsdsf  21982  prdsmet  21985  ressprdsds  21986  imasdsf1olem  21988  imasf1oxmet  21990  imasf1omet  21991  blfvalps  21998  xmetresbl  22052  metss2  22127  comet  22128  stdbdmet  22131  stdbdmopn  22133  methaus  22135  met2ndci  22137  metustfbas  22172  nrmmetd  22189  subgngp  22249  ngptgp  22250  sranlm  22298  nlmvscnlem1  22300  nlmvscn  22301  nrginvrcn  22306  lssnlm  22315  nghmcn  22359  qtopbaslem  22372  reconn  22439  xmetdcn2  22448  metdscn  22467  metnrm  22473  elcncf1di  22506  cncffvrn  22509  mulc1cncf  22516  cncfco  22518  reparphti  22605  isncvsngpd  22758  tchcph  22844  ipcnlem1  22852  ipcn  22853  iscfil3  22879  bcthlem5  22933  rrxmet  22999  minveclem3  23008  minveclem7  23014  ovolicc2lem4  23095  dyadmbl  23174  volcn  23180  itg1addlem1  23265  itg1addlem2  23270  itg1addlem4  23272  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  dvmptfsum  23542  c1liplem1  23563  dvgt0lem2  23570  ftc1a  23604  ply1domn  23687  ply1divmo  23699  fta1b  23733  ig1peu  23735  coeeu  23785  plydivalg  23858  aaliou2b  23900  ulmss  23955  ulmcn  23957  efif1olem4  24095  efsubm  24101  logccv  24209  logbmpt  24326  logbfval  24328  cvxcl  24511  basellem4  24610  fsumdvdscom  24711  musum  24717  dvdsmulf1o  24720  fsumdvdsmul  24721  dchrelbasd  24764  dchrmulcl  24774  dchrinv  24786  lgsqrlem2  24872  lgsdchr  24880  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  dchrisumlema  24977  dchrisumlem2  24979  chpdifbndlem2  25043  pntpbnd  25077  pntibndlem3  25081  axtgcont  25168  iscgrglt  25209  ercgrg  25212  idmot  25232  motco  25235  cnvmot  25236  motcgrg  25239  tgisline  25322  tghilberti2  25333  mirreu3  25349  mirmot  25370  ragperp  25412  foot  25414  mideu  25430  midf  25468  lmimot  25490  trgcopyeu  25498  f1otrgds  25549  f1otrg  25551  f1otrge  25552  xmstrkgc  25566  brbtwn2  25585  axlowdimlem15  25636  axcontlem2  25645  axcontlem10  25653  eengtrkg  25665  eengtrkge  25666  usgraedgreu  25917  usgraidx2v  25922  wlknwwlkninj  26239  wlkiswwlkinj  26246  wwlkextinj  26258  clwwlkf1  26324  clwlkf1clwwlk  26377  2spotiundisj  26589  2spotmdisj  26595  numclwlk1lem2f1  26621  grpoinvf  26770  nvmf  26884  vacn  26933  nmcvcn  26934  smcnlem  26936  sspg  26967  ssps  26969  sspmlem  26971  0lno  27029  blocni  27044  sspph  27094  ipblnfi  27095  minvecolem7  27123  unopf1o  28159  cnvunop  28161  unoplin  28163  counop  28164  hmopadj2  28184  hmoplin  28185  bralnfn  28191  lnopeq0i  28250  hmops  28263  hmopm  28264  hmopco  28266  lnconi  28276  cnlnadjlem2  28311  adjmul  28335  adjadd  28336  cdjreui  28675  disjxpin  28783  off2  28823  f1od2  28887  xrofsup  28923  odutos  28994  abliso  29027  archiabllem1  29078  archiabllem2  29082  suborng  29146  xrge0slmod  29175  1smat1  29198  submateq  29203  madjusmdetlem3  29223  pstmxmet  29268  ofcf  29492  ldgenpisys  29556  rossros  29570  inelcarsg  29700  sibfof  29729  sitmf  29741  erdszelem4  30430  erdszelem9  30435  erdsze2lem2  30440  cnpcon  30466  pconcon  30467  txpcon  30468  ptpcon  30469  cvxpcon  30478  cvxscon  30479  iccllyscon  30486  cvmseu  30512  cvmliftmo  30520  cvmlift2lem5  30543  cvmlift2lem9  30547  mrsubff1  30665  elmrsubrn  30671  mrsubco  30672  msubff1  30707  mvhf1  30710  segconeu  31288  fnessref  31522  neibastop1  31524  filnetlem3  31545  onsuct0  31610  unblimceq0lem  31667  unbdqndv2  31672  knoppndv  31695  uncf  32558  fin2so  32566  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  poimirlem26  32605  heicant  32614  mblfinlem2  32617  ftc1anc  32663  sdclem1  32709  isbnd3  32753  prdsbnd  32762  ismtycnv  32771  ismtyhmeolem  32773  ismtyres  32777  bfplem1  32791  bfplem2  32792  bfp  32793  rrnmet  32798  ismrer1  32807  iccbnd  32809  grpokerinj  32862  isdrngo2  32927  rngogrphom  32940  rngohomco  32943  rngoisocnv  32950  iscringd  32967  erprt  33176  lfl0f  33374  lkrlss  33400  lshpsmreu  33414  linepsubN  34056  pmapsub  34072  lautcnv  34394  lautco  34401  idltrn  34454  cdleme50f1  34849  cdleme50laut  34853  istendod  35068  dihf11  35574  dih1dimatlem  35636  lcfl7N  35808  lcfrlem9  35857  mapd1o  35955  hdmapf1oN  36175  hgmapf1oN  36213  nacsfix  36293  rmxypairf1o  36494  wepwsolem  36630  dnnumch3  36635  fnwe2  36641  mpaaeu  36739  idomsubgmo  36795  mon1psubm  36803  deg1mhm  36804  isotone1  37366  isotone2  37367  disjxp1  38263  disjf1  38364  wessf1ornlem  38366  projf1o  38381  sumnnodd  38697  lptioo2  38698  lptioo1  38699  cncfshift  38759  cncfperiod  38764  dvnprodlem1  38836  fourierdlem42  39042  nnfoctbdjlem  39348  isomennd  39421  smflimlem6  39662  iccpartgt  39965  icceuelpart  39974  otiunsndisjX  40317  usgredgreu  40445  uspgredg2vtxeu  40447  uspgredg2v  40451  usgredg2v  40454  1wlkpwwlkf1ouspgr  41076  wlknwwlksninj  41086  wlkwwlkinj  41093  wwlksnextinj  41105  clwwlksf1  41224  clwlksf1clwwlk  41276  frgrncvvdeq  41480  av-numclwlk1lem2f1  41524  ismgmd  41566  mgmhmpropd  41575  mgmhmf1o  41577  idmgmhm  41578  issubmgm2  41580  rabsubmgmd  41581  resmgmhm  41588  resmgmhm2  41589  resmgmhm2b  41590  mgmhmco  41591  submgmacs  41594  opmpt2ismgm  41597  mgmplusgiopALT  41620  isrnghm2d  41691  c0mgm  41699  c0mhm  41700  lidlmmgm  41715  2zlidl  41724  rnghmsscmap2  41765  rnghmsscmap  41766  rnghmsubcsetclem2  41768  rhmsscmap2  41811  rhmsscmap  41812  rhmsubcsetclem2  41814  rhmsscrnghm  41818  rhmsubcrngclem2  41820  srhmsubc  41868  fldhmsubc  41876  rhmsubc  41882  srhmsubcALTV  41887  fldhmsubcALTV  41895  rhmsubcALTV  41901  lindslinindsimp1  42040
  Copyright terms: Public domain W3C validator