Theorem ralrimivva 3181

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

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)
2	1	ex 412	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 3179	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3046

This theorem is referenced by:  disjord  5099  disjxiun  5107  otsndisj  5482  otiunsndisj  5483  swopo  5560  issod  5584  reuop  6269  fcof1  7265  fliftfund  7291  isof1oidb  7302  isof1oopb  7303  soisores  7305  soisoi  7306  isocnv  7308  f1oiso  7329  oveqrspc2v  7417  oprres  7560  caovclg  7584  caovcomg  7587  off  7674  coof  7680  caofidlcan  7694  caofrss  7695  caonncan  7700  dmmpog  8056  fnmpoovd  8069  fmpoco  8077  fsplitfpar  8100  poxp  8110  fvmpocurryd  8253  smo11  8336  smoiso2  8341  omsmo  8625  nnasmo  8630  coflton  8638  qsdisj2  8771  eroprf  8791  dom2lem  8966  omxpenlem  9047  xpf1o  9109  unxpdomlem3  9206  fofinf1o  9290  dffi3  9389  supmo  9410  infmo  9455  inf3lem6  9593  cantnf  9653  rankxplim  9839  fseqenlem1  9984  fodomacn  10016  iunfictbso  10074  cofsmo  10229  infpssrlem5  10267  enfin2i  10281  fin23lem23  10286  fin23lem27  10288  fin23lem28  10300  compssiso  10334  ltordlem  11710  cju  12189  axdc4uzlem  13955  seqcaopr2  14010  seqhomo  14021  wrd2ind  14695  cshf1  14782  s3sndisj  14940  s3iunsndisj  14941  climcn2  15566  addcn2  15567  mulcn2  15569  o1of2  15586  isercolllem1  15638  fsum2dlem  15743  fsumcom2  15747  fprodser  15922  fprod2dlem  15953  fprodcom2  15957  isprm6  16691  crth  16755  eulerthlem2  16759  vdwlem12  16970  cshwsdisj  17076  imasaddfnlem  17498  imasvscafn  17507  mreexexd  17616  iscatd  17641  oppccomfpropd  17695  isofn  17744  sectmon  17751  ssctr  17794  ssceq  17795  catsubcat  17808  issubc3  17818  fullsubc  17819  fullresc  17820  isfuncd  17834  idfucl  17850  cofucl  17857  funcres2b  17866  fulloppc  17893  fthoppc  17894  idffth  17904  cofull  17905  cofth  17906  ressffth  17909  setcmon  18056  setcepi  18057  resssetc  18061  resscatc  18078  catciso  18080  fthestrcsetc  18118  fullestrcsetc  18119  embedsetcestrclem  18125  fthsetcestrc  18133  fullsetcestrc  18134  evlfcl  18190  uncfcurf  18207  hofcl  18227  yonedalem3  18248  yonedainv  18249  yonffthlem  18250  yoniso  18253  isdrs2  18274  isposd  18290  pospropd  18293  poslubmo  18377  posglbmo  18378  mgmplusf  18584  ismgmd  18586  issstrmgm  18587  opifismgm  18593  mgmhmpropd  18632  mgmhmf1o  18634  idmgmhm  18635  issubmgm2  18637  rabsubmgmd  18638  resmgmhm  18645  resmgmhm2  18646  resmgmhm2b  18647  mgmhmco  18648  submgmacs  18651  issgrpd  18664  sgrppropd  18665  ismndd  18690  mndpropd  18693  issubmnd  18695  mndinvmod  18698  ismhmd  18720  mhmpropd  18726  idmhm  18729  mhmf1o  18730  issubmd  18740  mndissubm  18741  0mhm  18753  resmhm  18754  resmhm2  18755  resmhm2b  18756  mhmco  18757  submacs  18761  prdspjmhm  18763  pwsdiagmhm  18765  pwsco1mhm  18766  pwsco2mhm  18767  gsumwspan  18780  frmdsssubm  18795  frmdup1  18798  grpsubf  18958  dfgrp3  18978  mhmmnd  19003  mhmfmhm  19004  issubg4  19084  grpissubg  19085  isnsg3  19099  nsgacs  19101  0nsg  19108  nsgid  19109  qus0subgadd  19138  cycsubmcom  19143  isghmd  19164  ghmmhm  19165  idghm  19170  ghmnsgima  19179  ghmnsgpreima  19180  ghmf1  19185  kerf1ghm  19186  ghmf1o  19187  gaid  19238  subgga  19239  gass  19240  gasubg  19241  cntzsgrpcl  19273  cntzsubm  19277  cntrsubgnsg  19282  lactghmga  19342  symgfixf1  19374  odf1  19499  sylow1lem2  19536  sylow2blem2  19558  sylow3lem1  19564  lsmssv  19580  smndlsmidm  19593  pj1eu  19633  efglem  19653  efgtf  19659  efgred  19685  efgredeu  19689  frgpmhm  19702  frgpuptf  19707  frgpuplem  19709  mulgmhm  19764  ghmcmn  19768  invghm  19770  ablnsg  19784  imasabl  19813  cygabl  19828  gsum2d2lem  19910  gsum2d2  19911  gsumcom2  19912  dprd2d2  19983  ablfaclem2  20025  srgfcl  20112  srgcom4lem  20129  srglmhm  20137  srgrmhm  20138  ringcomlem  20195  isrnghm2d  20366  c0mgm  20375  c0mhm  20376  isrhm2d  20403  subrngringnsg  20469  issubrng2  20474  subrngint  20476  issubrg2  20508  subrgint  20511  rnghmsscmap2  20545  rnghmsscmap  20546  rnghmsubcsetclem2  20548  rhmsscmap2  20574  rhmsscmap  20575  rhmsubcsetclem2  20577  rhmsscrnghm  20581  rhmsubcrngclem2  20583  srhmsubc  20596  rhmsubc  20605  fldhmsubc  20701  primefld  20721  abvn0b  20752  islmodd  20779  lmodscaf  20797  lmodprop2d  20837  islssd  20848  islss4  20875  lssacs  20880  lsspropd  20931  islmhmd  20953  lmhmima  20961  lmhmpreima  20962  reslmhm  20966  lspextmo  20970  lsmcl  20997  pj1lmhm  21014  islbs2  21071  issubrgd  21103  dflidl2rng  21135  rnglidlmmgm  21162  rhmpreimaidl  21194  rngqiprnglin  21219  expmhm  21360  nn0srg  21361  prmirredlem  21389  expghm  21392  mulgghm2  21393  domnchr  21449  znf1o  21468  zntoslem  21473  znfld  21477  cygznlem3  21486  phlipf  21568  dsmmlss  21660  uvcf1  21708  frlmlbs  21713  lindff1  21736  lindfrn  21737  f1lindf  21738  issubassa2  21808  mvrf1  21902  mplsubglem  21915  mplsubrg  21921  mplcoe5lem  21953  mplcoe2  21955  mplind  21984  evlslem2  21993  evlseu  21997  mhplss  22049  ply1sclf1  22182  evls1maplmhm  22271  mamucl  22295  mamuass  22296  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  matbas2d  22317  mamumat1cl  22333  mamulid  22335  mamurid  22336  mat1mhm  22378  dmatid  22389  dmatsubcl  22392  dmatsgrp  22393  dmatmulcl  22394  dmatsrng  22395  dmatcrng  22396  scmatscmiddistr  22402  scmatscm  22407  scmatsgrp  22413  scmatsrng  22414  scmatcrng  22415  scmatsgrp1  22416  scmatsrng1  22417  scmatf1  22425  scmatmhm  22428  mavmul0g  22447  mdet1  22495  mdetunilem9  22514  mdetuni0  22515  mdetmul  22517  madutpos  22536  smadiadetlem4  22563  1elcpmat  22609  cpmatacl  22610  cpmatmcl  22613  mat2pmatf1  22623  mat2pmatmul  22625  mat2pmat1  22626  mat2pmatlin  22629  m2cpm  22635  m2cpminvid  22647  m2cpminvid2  22649  decpmatmul  22666  pmatcollpw1  22670  monmatcollpw  22673  pmatcollpw  22675  pmatcollpw3lem  22677  pmatcollpwscmatlem2  22684  pm2mpf1  22693  mp2pm2mplem4  22703  pm2mpmhmlem2  22713  chp0mat  22740  chpidmat  22741  tgclb  22864  mretopd  22986  toponmre  22987  iscldtop  22989  ordtbaslem  23082  ordtbas2  23085  cnt0  23240  haust1  23246  cnhaus  23248  isreg2  23271  dishaus  23276  ordthaus  23278  dfconn2  23313  iunconn  23322  clsconn  23324  2ndcomap  23352  dis2ndc  23354  llynlly  23371  restnlly  23376  restlly  23377  islly2  23378  llyidm  23382  nllyidm  23383  hausllycmp  23388  kgentopon  23432  txbas  23461  ptbasin2  23472  ptbasfi  23475  txcnp  23514  txcnmpt  23518  pthaus  23532  tx1stc  23544  xkococnlem  23553  xkococn  23554  cnmpt21  23565  qtoptop2  23593  qtopeu  23610  kqt0lem  23630  isr0  23631  regr1lem2  23634  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  nrmr0reg  23643  reghmph  23687  nrmhmph  23688  txswaphmeo  23699  qtophmeo  23711  fbun  23734  trfbas2  23737  isfil2  23750  infil  23757  trfil2  23781  filssufilg  23805  hausflim  23875  fclsnei  23913  fclsfnflim  23921  flimfnfcls  23922  ptcmplem1  23946  clssubg  24003  tgpconncomp  24007  qustgplem  24015  tsmsfbas  24022  utoptop  24129  iducn  24177  cstucnd  24178  isxmetd  24221  isxmet2d  24222  xmettpos  24244  prdsdsf  24262  prdsmet  24265  ressprdsds  24266  imasdsf1olem  24268  imasf1oxmet  24270  imasf1omet  24271  blfvalps  24278  xmetresbl  24332  metss2  24407  comet  24408  stdbdmet  24411  stdbdmopn  24413  methaus  24415  met2ndci  24417  metustfbas  24452  nrmmetd  24469  subgngp  24530  ngptgp  24531  sranlm  24579  nlmvscnlem1  24581  nlmvscn  24582  nrginvrcn  24587  lssnlm  24596  nghmcn  24640  qtopbaslem  24653  reconn  24724  xmetdcn2  24733  metdscn  24752  metnrm  24758  elcncf1di  24795  cncfcdm  24798  mulc1cncf  24805  cncfco  24807  reparphti  24903  reparphtiOLD  24904  isncvsngpd  25057  tcphcph  25144  ipcnlem1  25152  ipcn  25153  iscfil3  25180  bcthlem5  25235  rrxmet  25315  minveclem3  25336  minveclem7  25342  ovolicc2lem4  25428  dyadmbl  25508  volcn  25514  itg1addlem1  25600  itg1addlem2  25605  itg1addlem4  25607  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  dvmptfsum  25886  c1liplem1  25908  dvgt0lem2  25915  ftc1a  25951  ply1domn  26036  ply1divmo  26048  fta1b  26084  ig1peu  26087  coeeu  26137  plydivalg  26214  aaliou2b  26256  ulmss  26313  ulmcn  26315  efif1olem4  26461  efsubm  26467  logccv  26579  logbmpt  26705  logbfval  26707  cvxcl  26902  basellem4  27001  fsumdvdscom  27102  musum  27108  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  dchrelbasd  27157  dchrmulcl  27167  dchrinv  27179  lgsqrlem2  27265  lgsdchr  27273  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  2sqreulem4  27372  dchrisumlema  27406  dchrisumlem2  27408  chpdifbndlem2  27472  pntpbnd  27506  pntibndlem3  27510  ssltd  27710  oldbday  27819  addsprop  27890  mulscutlem  28041  divsmo  28094  om2noseqf1o  28202  om2noseqiso  28203  axtgcont  28403  tgjustc1  28409  tgjustc2  28410  iscgrglt  28448  ercgrg  28451  idmot  28471  motco  28474  cnvmot  28475  motcgrg  28478  tgisline  28561  tghilberti2  28572  mirreu3  28588  mirmot  28609  ragperp  28651  foot  28656  mideu  28672  midf  28710  lmimot  28732  trgcopyeu  28740  f1otrgds  28803  f1otrg  28805  f1otrge  28806  xmstrkgc  28820  brbtwn2  28839  axlowdimlem15  28890  axcontlem2  28899  axcontlem10  28907  eengtrkg  28920  eengtrkge  28921  numedglnl  29078  usgredgreu  29152  uspgredg2vtxeu  29154  uspgredg2v  29158  usgredg2v  29161  wlkswwlksf1o  29816  wwlksnextinj  29836  clwlkclwwlkf1  29946  clwwlkf1  29985  frcond4  30206  frgrncvvdeqlem8  30242  frgrncvvdeq  30245  frgrwopreglem4  30251  numclwwlk1lem2f1  30293  nrt2irr  30409  grpoinvf  30468  nvmf  30581  vacn  30630  nmcvcn  30631  smcnlem  30633  sspg  30664  ssps  30666  sspmlem  30668  0lno  30726  blocni  30741  ipblnfi  30791  minvecolem7  30819  unopf1o  31852  cnvunop  31854  unoplin  31856  counop  31857  hmopadj2  31877  hmoplin  31878  bralnfn  31884  lnopeq0i  31943  hmops  31956  hmopm  31957  hmopco  31959  lnconi  31969  cnlnadjlem2  32004  adjmul  32028  adjadd  32029  cdjreui  32368  disjxpin  32524  off2  32572  2ndresdju  32580  fnpreimac  32602  suppovss  32611  f1od2  32651  xrofsup  32697  s3f1  32875  ccatf1  32877  swrdf1  32885  odutos  32901  dfmgc2lem  32928  dfmgc2  32929  pwrssmgc  32933  mgcf1o  32936  mndlactf1  32974  mndractf1  32976  abliso  32984  symgcntz  33049  tocyccntz  33108  conjga  33134  archiabllem1  33154  archiabllem2  33158  urpropd  33190  elrgspnlem2  33201  rlocf1  33231  rrgsubm  33241  subrdom  33242  suborng  33300  xrge0slmod  33326  nsgmgc  33390  intlidl  33398  idlinsubrg  33409  rhmimaidl  33410  prmidl2  33419  idlmulssprm  33420  isprmidlc  33425  rhmpreimaprmidl  33429  qsidomlem1  33430  qsidomlem2  33431  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  ssmxidllem  33451  rsprprmprmidl  33500  rsprprmprmidlb  33501  rprmirred  33509  rprmirredb  33510  1arithufdlem4  33525  ply1degltdimlem  33625  ply1degltdim  33626  lindsun  33628  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  lactlmhm  33637  assalactf1o  33638  minplyirred  33708  constrsdrg  33772  1smat1  33801  submateq  33806  madjusmdetlem3  33826  zart0  33876  pstmxmet  33894  ofcf  34100  ldgenpisys  34163  rossros  34177  inelcarsg  34309  sibfof  34338  sitmf  34350  hgt750lemb  34654  erdszelem4  35188  erdszelem9  35193  erdsze2lem2  35198  cnpconn  35224  pconnconn  35225  txpconn  35226  ptpconn  35227  cvxpconn  35236  cvxsconn  35237  iccllysconn  35244  cvmseu  35270  cvmliftmo  35278  cvmlift2lem5  35301  cvmlift2lem9  35305  mrsubff1  35508  elmrsubrn  35514  mrsubco  35515  msubff1  35550  mvhf1  35553  r1peuqusdeg1  35637  segconeu  36006  fnessref  36352  neibastop1  36354  filnetlem3  36375  onsuct0  36436  weiunlem2  36458  unblimceq0lem  36501  unbdqndv2  36506  knoppndv  36529  irrdiff  37321  uncf  37600  fin2so  37608  lindsadd  37614  poimirlem4  37625  poimirlem13  37634  poimirlem14  37635  poimirlem26  37647  heicant  37656  mblfinlem2  37659  ftc1anc  37702  sdclem1  37744  isbnd3  37785  prdsbnd  37794  ismtycnv  37803  ismtyhmeolem  37805  ismtyres  37809  bfplem1  37823  bfplem2  37824  bfp  37825  rrnmet  37830  ismrer1  37839  iccbnd  37841  grpokerinj  37894  isdrngo2  37959  rngogrphom  37972  rngohomco  37975  rngoisocnv  37982  iscringd  37999  eqvreldisj1  38823  erprt  38873  lfl0f  39069  lkrlss  39095  lshpsmreu  39109  linepsubN  39753  pmapsub  39769  lautcnv  40091  lautco  40098  idltrn  40151  cdleme50f1  40544  cdleme50laut  40548  istendod  40763  dihf11  41268  dih1dimatlem  41330  lcfl7N  41502  lcfrlem9  41551  mapd1o  41649  hdmapf1oN  41866  hgmapf1oN  41904  fmpocos  42229  qsalrel  42235  rediveud  42438  imacrhmcl  42509  evlselv  42582  fsuppind  42585  nacsfix  42707  rmxypairf1o  42907  wepwsolem  43038  dnnumch3  43043  fnwe2  43049  mpaaeu  43146  idomsubgmo  43189  mon1psubm  43195  deg1mhm  43196  isotone1  44044  isotone2  44045  mnringmulrcld  44224  traxext  44974  disjxp1  45070  disjf1  45184  wessf1ornlem  45186  projf1o  45198  sumnnodd  45635  lptioo2  45636  lptioo1  45637  cncfshift  45879  cncfperiod  45884  dvnprodlem1  45951  fourierdlem42  46154  nnfoctbdjlem  46460  isomennd  46536  smflimlem6  46781  fsetsnf1  47057  cfsetsnfsetf1  47064  otiunsndisjX  47284  imasetpreimafvbijlemf1  47409  iccpartgt  47432  icceuelpart  47441  ichnreuop  47477  sprsymrelfolem2  47498  sprsymrelf  47500  prproropf1o  47512  reupr  47527  reuopreuprim  47531  uhgrimprop  47896  isuspgrim0lem  47897  upgrimtrls  47910  gpgprismgr4cycllem11  48099  opmpoismgm  48159  mgmplusgiopALT  48186  2zlidl  48232  rhmsubcALTV  48277  srhmsubcALTV  48317  fldhmsubcALTV  48325  lindslinindsimp1  48450  1arymaptf1  48635  2arymaptf1  48646  eqfnovd  48858  fmpodg  48861  toslat  48974  catprsc  49006  catprsc2  49007  oppcendc  49011  invfn  49023  iinfssclem2  49048  iinfssc  49050  iinfsubc  49051  discsubc  49057  nelsubclem  49060  resccatlem  49066  funchomf  49090  imasubclem2  49098  imaidfu  49103  imasubc  49144  imassc  49146  imasubc3  49149  fthcomf  49150  idfth  49151  cofidfth  49155  upeu2  49165  isnatd  49216  swapfffth  49276  diag1f1  49300  diag2f1  49302  fucoppc  49403  isthincd  49429  isthincd2  49430  oppcthinco  49432  oppcthinendcALT  49434  functhinclem4  49440  functhincfun  49442  thincfth  49445  thincciso  49446  thinccisod  49447  functermc  49501  arweuthinc  49522  arweutermc  49523  diagffth  49531  funcsn  49534  0fucterm  49536