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

Theorem ralrimivva 3195
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 413 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 3194 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3147
This theorem is referenced by:  disjord  5050  disjxiun  5059  otsndisj  5405  otiunsndisj  5406  swopo  5482  issod  5504  reuop  6141  fcof1  7040  fliftfund  7061  isof1oidb  7072  isof1oopb  7073  soisores  7075  soisoi  7076  isocnv  7078  f1oiso  7099  oveqrspc2v  7178  oprres  7309  caovclg  7333  caovcomg  7336  off  7417  caofrss  7435  caonncan  7440  dmmpog  7766  fnmpoovd  7776  fmpoco  7784  fsplitfpar  7808  poxp  7816  fvmpocurryd  7931  smo11  7995  smoiso2  8000  omsmo  8274  qsdisj2  8368  eroprf  8388  dom2lem  8541  omxpenlem  8610  xpf1o  8671  unxpdomlem3  8716  fofinf1o  8791  dffi3  8887  supmo  8908  infmo  8951  inf3lem6  9088  cantnf  9148  rankxplim  9300  fseqenlem1  9442  fodomacn  9474  iunfictbso  9532  cofsmo  9683  infpssrlem5  9721  enfin2i  9735  fin23lem23  9740  fin23lem27  9742  fin23lem28  9754  compssiso  9788  ltordlem  11157  cju  11626  axdc4uzlem  13344  seqcaopr2  13399  seqhomo  13410  wrd2ind  14078  cshf1  14165  s3sndisj  14320  s3iunsndisj  14321  climcn2  14942  addcn2  14943  mulcn2  14945  o1of2  14962  isercolllem1  15014  fsum2dlem  15117  fsumcom2  15121  fprodser  15295  fprod2dlem  15326  fprodcom2  15330  isprm6  16050  crth  16107  eulerthlem2  16111  vdwlem12  16320  cshwsdisj  16424  imasaddfnlem  16793  imasvscafn  16802  mreexexd  16911  iscatd  16936  oppccomfpropd  16989  isofn  17037  sectmon  17044  ssctr  17087  ssceq  17088  catsubcat  17101  issubc3  17111  fullsubc  17112  fullresc  17113  isfuncd  17127  idfucl  17143  cofucl  17150  funcres2b  17159  fulloppc  17184  fthoppc  17185  idffth  17195  cofull  17196  cofth  17197  ressffth  17200  setcmon  17339  setcepi  17340  resssetc  17344  resscatc  17357  catciso  17359  fthestrcsetc  17392  fullestrcsetc  17393  embedsetcestrclem  17399  fthsetcestrc  17407  fullsetcestrc  17408  evlfcl  17464  uncfcurf  17481  hofcl  17501  yonedalem3  17522  yonedainv  17523  yonffthlem  17524  yoniso  17527  isdrs2  17541  isposd  17557  pospropd  17736  poslubmo  17748  posglbmo  17749  mgmplusf  17853  issstrmgm  17854  opifismgm  17860  ismndd  17923  mndpropd  17926  issubmnd  17928  mndinvmod  17931  mhmpropd  17952  idmhm  17955  mhmf1o  17956  issubmd  17960  0mhm  17969  resmhm  17970  resmhm2  17971  resmhm2b  17972  mhmco  17973  submacs  17976  prdspjmhm  17978  pwsdiagmhm  17980  pwsco1mhm  17981  pwsco2mhm  17982  gsumwspan  17996  frmdsssubm  18011  frmdup1  18014  grpsubf  18110  dfgrp3  18130  mhmmnd  18153  mhmfmhm  18154  issubg4  18230  grpissubg  18231  isnsg3  18244  nsgacs  18246  0nsg  18253  nsgid  18254  cycsubmcom  18279  isghmd  18299  ghmmhm  18300  idghm  18305  ghmnsgima  18314  ghmnsgpreima  18315  ghmf1  18319  ghmf1o  18320  gaid  18361  subgga  18362  gass  18363  gasubg  18364  cntzsubm  18398  cntrsubgnsg  18403  lactghmga  18454  symgfixf1  18487  odf1  18611  sylow1lem2  18646  sylow2blem2  18668  sylow3lem1  18674  lsmssv  18690  smndlsmidm  18703  lsmidmOLD  18711  pj1eu  18744  efglem  18764  efgtf  18770  efgred  18796  efgredeu  18800  frgpmhm  18813  frgpuptf  18818  frgpuplem  18820  mulgmhm  18870  ghmcmn  18874  invghm  18876  ablnsg  18889  cygabl  18932  gsum2d2lem  19015  gsum2d2  19016  gsumcom2  19017  dprd2d2  19088  ablfaclem2  19130  srgfcl  19187  srglmhm  19207  srgrmhm  19208  isrhm2d  19402  kerf1ghm  19419  kerf1hrmOLD  19420  issubrg2  19477  subrgint  19479  primefld  19506  islmodd  19562  lmodscaf  19578  lmodprop2d  19618  islssd  19629  islss4  19656  lssacs  19661  lsspropd  19711  islmhmd  19733  lmhmima  19741  lmhmpreima  19742  reslmhm  19746  lspextmo  19750  lsmcl  19777  pj1lmhm  19794  islbs2  19848  issubrngd2  19883  opprdomn  19995  abvn0b  19996  issubassa2  20042  mvrf1  20126  mplsubglem  20135  mplsubrg  20141  mplcoe5lem  20168  mplcoe2  20170  mplind  20202  evlslem2  20212  evlseu  20216  mhplss  20259  ply1sclf1  20374  expmhm  20530  nn0srg  20531  prmirredlem  20556  expghm  20559  mulgghm2  20560  domnchr  20595  znf1o  20614  zntoslem  20619  znfld  20623  cygznlem3  20632  phlipf  20712  dsmmlss  20804  uvcf1  20852  frlmlbs  20857  lindff1  20880  lindfrn  20881  f1lindf  20882  mamucl  20926  mamuass  20927  mamudi  20928  mamudir  20929  mamuvs1  20930  mamuvs2  20931  matbas2d  20948  mamumat1cl  20964  mamulid  20966  mamurid  20967  mat1mhm  21009  dmatid  21020  dmatsubcl  21023  dmatsgrp  21024  dmatmulcl  21025  dmatsrng  21026  dmatcrng  21027  scmatscmiddistr  21033  scmatscm  21038  scmatsgrp  21044  scmatsrng  21045  scmatcrng  21046  scmatsgrp1  21047  scmatsrng1  21048  scmatf1  21056  scmatmhm  21059  mavmul0g  21078  mdet1  21126  mdetunilem9  21145  mdetuni0  21146  mdetmul  21148  madutpos  21167  smadiadetlem4  21194  1elcpmat  21239  cpmatacl  21240  cpmatmcl  21243  mat2pmatf1  21253  mat2pmatmul  21255  mat2pmat1  21256  mat2pmatlin  21259  m2cpm  21265  m2cpminvid  21277  m2cpminvid2  21279  decpmatmul  21296  pmatcollpw1  21300  monmatcollpw  21303  pmatcollpw  21305  pmatcollpw3lem  21307  pmatcollpwscmatlem2  21314  pm2mpf1  21323  mp2pm2mplem4  21333  pm2mpmhmlem2  21343  chp0mat  21370  chpidmat  21371  tgclb  21494  mretopd  21616  toponmre  21617  iscldtop  21619  ordtbaslem  21712  ordtbas2  21715  cnt0  21870  haust1  21876  cnhaus  21878  isreg2  21901  dishaus  21906  ordthaus  21908  dfconn2  21943  iunconn  21952  clsconn  21954  2ndcomap  21982  dis2ndc  21984  llynlly  22001  restnlly  22006  restlly  22007  islly2  22008  llyidm  22012  nllyidm  22013  hausllycmp  22018  kgentopon  22062  txbas  22091  ptbasin2  22102  ptbasfi  22105  txcnp  22144  txcnmpt  22148  pthaus  22162  tx1stc  22174  xkococnlem  22183  xkococn  22184  cnmpt21  22195  qtoptop2  22223  qtopeu  22240  kqt0lem  22260  isr0  22261  regr1lem2  22264  kqreglem1  22265  kqreglem2  22266  kqnrmlem1  22267  kqnrmlem2  22268  nrmr0reg  22273  reghmph  22317  nrmhmph  22318  txswaphmeo  22329  qtophmeo  22341  fbun  22364  trfbas2  22367  isfil2  22380  infil  22387  trfil2  22411  filssufilg  22435  hausflim  22505  fclsnei  22543  fclsfnflim  22551  flimfnfcls  22552  ptcmplem1  22576  clssubg  22632  tgpconncomp  22636  qustgplem  22644  tsmsfbas  22651  utoptop  22758  iducn  22807  cstucnd  22808  isxmetd  22851  isxmet2d  22852  xmettpos  22874  prdsdsf  22892  prdsmet  22895  ressprdsds  22896  imasdsf1olem  22898  imasf1oxmet  22900  imasf1omet  22901  blfvalps  22908  xmetresbl  22962  metss2  23037  comet  23038  stdbdmet  23041  stdbdmopn  23043  methaus  23045  met2ndci  23047  metustfbas  23082  nrmmetd  23099  subgngp  23159  ngptgp  23160  sranlm  23208  nlmvscnlem1  23210  nlmvscn  23211  nrginvrcn  23216  lssnlm  23225  nghmcn  23269  qtopbaslem  23282  reconn  23351  xmetdcn2  23360  metdscn  23379  metnrm  23385  elcncf1di  23418  cncffvrn  23421  mulc1cncf  23428  cncfco  23430  reparphti  23516  isncvsngpd  23669  tcphcph  23755  ipcnlem1  23763  ipcn  23764  iscfil3  23791  bcthlem5  23846  rrxmet  23926  minveclem3  23947  minveclem7  23953  ovolicc2lem4  24036  dyadmbl  24116  volcn  24122  itg1addlem1  24208  itg1addlem2  24213  itg1addlem4  24215  mbfi1fseqlem1  24231  mbfi1fseqlem3  24233  mbfi1fseqlem4  24234  mbfi1fseqlem5  24235  dvmptfsum  24487  c1liplem1  24508  dvgt0lem2  24515  ftc1a  24549  ply1domn  24632  ply1divmo  24644  fta1b  24678  ig1peu  24680  coeeu  24730  plydivalg  24803  aaliou2b  24845  ulmss  24900  ulmcn  24902  efif1olem4  25042  efsubm  25048  logccv  25159  logbmpt  25279  logbfval  25281  cvxcl  25476  basellem4  25575  fsumdvdscom  25676  musum  25682  dvdsmulf1o  25685  fsumdvdsmul  25686  dchrelbasd  25729  dchrmulcl  25739  dchrinv  25751  lgsqrlem2  25837  lgsdchr  25845  lgseisenlem2  25866  lgsquadlem1  25870  lgsquadlem2  25871  2sqreulem4  25944  dchrisumlema  25978  dchrisumlem2  25980  chpdifbndlem2  26044  pntpbnd  26078  pntibndlem3  26082  axtgcont  26169  tgjustc1  26175  tgjustc2  26176  iscgrglt  26214  ercgrg  26217  idmot  26237  motco  26240  cnvmot  26241  motcgrg  26244  tgisline  26327  tghilberti2  26338  mirreu3  26354  mirmot  26375  ragperp  26417  foot  26422  mideu  26438  midf  26476  lmimot  26498  trgcopyeu  26506  f1otrgds  26569  f1otrg  26571  f1otrge  26572  xmstrkgc  26586  brbtwn2  26605  axlowdimlem15  26656  axcontlem2  26665  axcontlem10  26673  eengtrkg  26686  eengtrkge  26687  numedglnl  26843  usgredgreu  26914  uspgredg2vtxeu  26916  uspgredg2v  26920  usgredg2v  26923  wlkswwlksf1o  27571  wwlksnextinj  27591  clwlkclwwlkf1  27702  clwwlkf1  27742  frcond4  27963  frgrncvvdeqlem8  27999  frgrncvvdeq  28002  frgrwopreglem4  28008  numclwwlk1lem2f1  28050  grpoinvf  28223  nvmf  28336  vacn  28385  nmcvcn  28386  smcnlem  28388  sspg  28419  ssps  28421  sspmlem  28423  0lno  28481  blocni  28496  ipblnfi  28546  minvecolem7  28574  unopf1o  29607  cnvunop  29609  unoplin  29611  counop  29612  hmopadj2  29632  hmoplin  29633  bralnfn  29639  lnopeq0i  29698  hmops  29711  hmopm  29712  hmopco  29714  lnconi  29724  cnlnadjlem2  29759  adjmul  29783  adjadd  29784  cdjreui  30123  disjxpin  30253  off2  30303  fnpreimac  30331  suppovss  30341  f1od2  30370  xrofsup  30405  s3f1  30537  ccatf1  30539  swrdf1  30544  odutos  30564  abliso  30597  symgcntz  30643  tocyccntz  30700  archiabllem1  30736  archiabllem2  30740  suborng  30802  xrge0slmod  30831  prmidl2  30864  isprmidlc  30868  qsidomlem1  30869  qsidomlem2  30870  lindsun  30907  fedgmullem1  30911  fedgmullem2  30912  fedgmul  30913  1smat1  30955  submateq  30960  madjusmdetlem3  30980  pstmxmet  31023  ofcf  31248  ldgenpisys  31311  rossros  31325  inelcarsg  31455  sibfof  31484  sitmf  31496  hgt750lemb  31813  erdszelem4  32325  erdszelem9  32330  erdsze2lem2  32335  cnpconn  32361  pconnconn  32362  txpconn  32363  ptpconn  32364  cvxpconn  32373  cvxsconn  32374  iccllysconn  32381  cvmseu  32407  cvmliftmo  32415  cvmlift2lem5  32438  cvmlift2lem9  32442  mrsubff1  32645  elmrsubrn  32651  mrsubco  32652  msubff1  32687  mvhf1  32690  sslttr  33152  segconeu  33356  fnessref  33589  neibastop1  33591  filnetlem3  33612  onsuct0  33673  unblimceq0lem  33729  unbdqndv2  33734  knoppndv  33757  uncf  34738  fin2so  34746  lindsadd  34752  poimirlem4  34763  poimirlem13  34772  poimirlem14  34773  poimirlem26  34785  heicant  34794  mblfinlem2  34797  ftc1anc  34842  sdclem1  34886  isbnd3  34930  prdsbnd  34939  ismtycnv  34948  ismtyhmeolem  34950  ismtyres  34954  bfplem1  34968  bfplem2  34969  bfp  34970  rrnmet  34975  ismrer1  34984  iccbnd  34986  grpokerinj  35039  isdrngo2  35104  rngogrphom  35117  rngohomco  35120  rngoisocnv  35127  iscringd  35144  erprt  35876  lfl0f  36072  lkrlss  36098  lshpsmreu  36112  linepsubN  36755  pmapsub  36771  lautcnv  37093  lautco  37100  idltrn  37153  cdleme50f1  37546  cdleme50laut  37550  istendod  37765  dihf11  38270  dih1dimatlem  38332  lcfl7N  38504  lcfrlem9  38553  mapd1o  38651  hdmapf1oN  38868  hgmapf1oN  38906  qsalrel  38990  nacsfix  39170  rmxypairf1o  39369  wepwsolem  39503  dnnumch3  39508  fnwe2  39514  mpaaeu  39611  idomsubgmo  39659  mon1psubm  39667  deg1mhm  39668  isotone1  40259  isotone2  40260  disjxp1  41192  disjf1  41304  wessf1ornlem  41306  projf1o  41320  sumnnodd  41772  lptioo2  41773  lptioo1  41774  cncfshift  42018  cncfperiod  42023  dvnprodlem1  42092  fourierdlem42  42296  nnfoctbdjlem  42599  isomennd  42675  smflimlem6  42914  otiunsndisjX  43340  iccpartgt  43415  icceuelpart  43424  ichnreuop  43462  sprsymrelfolem2  43483  sprsymrelf  43485  prproropf1o  43497  reupr  43512  reuopreuprim  43516  isomuspgrlem2c  43823  isomuspgr  43827  ismgmd  43871  mgmhmpropd  43880  mgmhmf1o  43882  idmgmhm  43883  issubmgm2  43885  rabsubmgmd  43886  resmgmhm  43893  resmgmhm2  43894  resmgmhm2b  43895  mgmhmco  43896  submgmacs  43899  opmpoismgm  43902  mgmplusgiopALT  43929  isrnghm2d  44000  c0mgm  44008  c0mhm  44009  lidlmmgm  44024  2zlidl  44033  rnghmsscmap2  44072  rnghmsscmap  44073  rnghmsubcsetclem2  44075  rhmsscmap2  44118  rhmsscmap  44119  rhmsubcsetclem2  44121  rhmsscrnghm  44125  rhmsubcrngclem2  44127  srhmsubc  44175  fldhmsubc  44183  rhmsubc  44189  srhmsubcALTV  44193  fldhmsubcALTV  44201  rhmsubcALTV  44207  lindslinindsimp1  44340
  Copyright terms: Public domain W3C validator