Theorem ralrimivva 3187

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 3185	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051

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 3052

This theorem is referenced by:  disjord  5108  disjxiun  5116  otsndisj  5494  otiunsndisj  5495  swopo  5572  issod  5596  reuop  6282  fcof1  7279  fliftfund  7305  isof1oidb  7316  isof1oopb  7317  soisores  7319  soisoi  7320  isocnv  7322  f1oiso  7343  oveqrspc2v  7430  oprres  7573  caovclg  7597  caovcomg  7600  off  7687  coof  7693  caofidlcan  7707  caofrss  7708  caonncan  7713  dmmpog  8071  fnmpoovd  8084  fmpoco  8092  fsplitfpar  8115  poxp  8125  fvmpocurryd  8268  smo11  8376  smoiso2  8381  omsmo  8668  nnasmo  8673  coflton  8681  qsdisj2  8807  eroprf  8827  dom2lem  9004  omxpenlem  9085  xpf1o  9151  unxpdomlem3  9258  fofinf1o  9342  dffi3  9441  supmo  9462  infmo  9507  inf3lem6  9645  cantnf  9705  rankxplim  9891  fseqenlem1  10036  fodomacn  10068  iunfictbso  10126  cofsmo  10281  infpssrlem5  10319  enfin2i  10333  fin23lem23  10338  fin23lem27  10340  fin23lem28  10352  compssiso  10386  ltordlem  11760  cju  12234  axdc4uzlem  13999  seqcaopr2  14054  seqhomo  14065  wrd2ind  14739  cshf1  14826  s3sndisj  14984  s3iunsndisj  14985  climcn2  15607  addcn2  15608  mulcn2  15610  o1of2  15627  isercolllem1  15679  fsum2dlem  15784  fsumcom2  15788  fprodser  15963  fprod2dlem  15994  fprodcom2  15998  isprm6  16731  crth  16795  eulerthlem2  16799  vdwlem12  17010  cshwsdisj  17116  imasaddfnlem  17540  imasvscafn  17549  mreexexd  17658  iscatd  17683  oppccomfpropd  17737  isofn  17786  sectmon  17793  ssctr  17836  ssceq  17837  catsubcat  17850  issubc3  17860  fullsubc  17861  fullresc  17862  isfuncd  17876  idfucl  17892  cofucl  17899  funcres2b  17908  fulloppc  17935  fthoppc  17936  idffth  17946  cofull  17947  cofth  17948  ressffth  17951  setcmon  18098  setcepi  18099  resssetc  18103  resscatc  18120  catciso  18122  fthestrcsetc  18160  fullestrcsetc  18161  embedsetcestrclem  18167  fthsetcestrc  18175  fullsetcestrc  18176  evlfcl  18232  uncfcurf  18249  hofcl  18269  yonedalem3  18290  yonedainv  18291  yonffthlem  18292  yoniso  18295  isdrs2  18316  isposd  18332  pospropd  18335  poslubmo  18419  posglbmo  18420  mgmplusf  18626  ismgmd  18628  issstrmgm  18629  opifismgm  18635  mgmhmpropd  18674  mgmhmf1o  18676  idmgmhm  18677  issubmgm2  18679  rabsubmgmd  18680  resmgmhm  18687  resmgmhm2  18688  resmgmhm2b  18689  mgmhmco  18690  submgmacs  18693  issgrpd  18706  sgrppropd  18707  ismndd  18732  mndpropd  18735  issubmnd  18737  mndinvmod  18740  ismhmd  18762  mhmpropd  18768  idmhm  18771  mhmf1o  18772  issubmd  18782  mndissubm  18783  0mhm  18795  resmhm  18796  resmhm2  18797  resmhm2b  18798  mhmco  18799  submacs  18803  prdspjmhm  18805  pwsdiagmhm  18807  pwsco1mhm  18808  pwsco2mhm  18809  gsumwspan  18822  frmdsssubm  18837  frmdup1  18840  grpsubf  19000  dfgrp3  19020  mhmmnd  19045  mhmfmhm  19046  issubg4  19126  grpissubg  19127  isnsg3  19141  nsgacs  19143  0nsg  19150  nsgid  19151  qus0subgadd  19180  cycsubmcom  19185  isghmd  19206  ghmmhm  19207  idghm  19212  ghmnsgima  19221  ghmnsgpreima  19222  ghmf1  19227  kerf1ghm  19228  ghmf1o  19229  gaid  19280  subgga  19281  gass  19282  gasubg  19283  cntzsgrpcl  19315  cntzsubm  19319  cntrsubgnsg  19324  lactghmga  19384  symgfixf1  19416  odf1  19541  sylow1lem2  19578  sylow2blem2  19600  sylow3lem1  19606  lsmssv  19622  smndlsmidm  19635  pj1eu  19675  efglem  19695  efgtf  19701  efgred  19727  efgredeu  19731  frgpmhm  19744  frgpuptf  19749  frgpuplem  19751  mulgmhm  19806  ghmcmn  19810  invghm  19812  ablnsg  19826  imasabl  19855  cygabl  19870  gsum2d2lem  19952  gsum2d2  19953  gsumcom2  19954  dprd2d2  20025  ablfaclem2  20067  srgfcl  20154  srgcom4lem  20171  srglmhm  20179  srgrmhm  20180  ringcomlem  20237  isrnghm2d  20408  c0mgm  20417  c0mhm  20418  isrhm2d  20445  subrngringnsg  20511  issubrng2  20516  subrngint  20518  issubrg2  20550  subrgint  20553  rnghmsscmap2  20587  rnghmsscmap  20588  rnghmsubcsetclem2  20590  rhmsscmap2  20616  rhmsscmap  20617  rhmsubcsetclem2  20619  rhmsscrnghm  20623  rhmsubcrngclem2  20625  srhmsubc  20638  rhmsubc  20647  fldhmsubc  20743  primefld  20763  abvn0b  20794  islmodd  20821  lmodscaf  20839  lmodprop2d  20879  islssd  20890  islss4  20917  lssacs  20922  lsspropd  20973  islmhmd  20995  lmhmima  21003  lmhmpreima  21004  reslmhm  21008  lspextmo  21012  lsmcl  21039  pj1lmhm  21056  islbs2  21113  issubrgd  21145  dflidl2rng  21177  rnglidlmmgm  21204  rhmpreimaidl  21236  rngqiprnglin  21261  expmhm  21402  nn0srg  21403  prmirredlem  21431  expghm  21434  mulgghm2  21435  domnchr  21491  znf1o  21510  zntoslem  21515  znfld  21519  cygznlem3  21528  phlipf  21610  dsmmlss  21702  uvcf1  21750  frlmlbs  21755  lindff1  21778  lindfrn  21779  f1lindf  21780  issubassa2  21850  mvrf1  21944  mplsubglem  21957  mplsubrg  21963  mplcoe5lem  21995  mplcoe2  21997  mplind  22026  evlslem2  22035  evlseu  22039  mhplss  22091  ply1sclf1  22224  evls1maplmhm  22313  mamucl  22337  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  matbas2d  22359  mamumat1cl  22375  mamulid  22377  mamurid  22378  mat1mhm  22420  dmatid  22431  dmatsubcl  22434  dmatsgrp  22435  dmatmulcl  22436  dmatsrng  22437  dmatcrng  22438  scmatscmiddistr  22444  scmatscm  22449  scmatsgrp  22455  scmatsrng  22456  scmatcrng  22457  scmatsgrp1  22458  scmatsrng1  22459  scmatf1  22467  scmatmhm  22470  mavmul0g  22489  mdet1  22537  mdetunilem9  22556  mdetuni0  22557  mdetmul  22559  madutpos  22578  smadiadetlem4  22605  1elcpmat  22651  cpmatacl  22652  cpmatmcl  22655  mat2pmatf1  22665  mat2pmatmul  22667  mat2pmat1  22668  mat2pmatlin  22671  m2cpm  22677  m2cpminvid  22689  m2cpminvid2  22691  decpmatmul  22708  pmatcollpw1  22712  monmatcollpw  22715  pmatcollpw  22717  pmatcollpw3lem  22719  pmatcollpwscmatlem2  22726  pm2mpf1  22735  mp2pm2mplem4  22745  pm2mpmhmlem2  22755  chp0mat  22782  chpidmat  22783  tgclb  22906  mretopd  23028  toponmre  23029  iscldtop  23031  ordtbaslem  23124  ordtbas2  23127  cnt0  23282  haust1  23288  cnhaus  23290  isreg2  23313  dishaus  23318  ordthaus  23320  dfconn2  23355  iunconn  23364  clsconn  23366  2ndcomap  23394  dis2ndc  23396  llynlly  23413  restnlly  23418  restlly  23419  islly2  23420  llyidm  23424  nllyidm  23425  hausllycmp  23430  kgentopon  23474  txbas  23503  ptbasin2  23514  ptbasfi  23517  txcnp  23556  txcnmpt  23560  pthaus  23574  tx1stc  23586  xkococnlem  23595  xkococn  23596  cnmpt21  23607  qtoptop2  23635  qtopeu  23652  kqt0lem  23672  isr0  23673  regr1lem2  23676  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  nrmr0reg  23685  reghmph  23729  nrmhmph  23730  txswaphmeo  23741  qtophmeo  23753  fbun  23776  trfbas2  23779  isfil2  23792  infil  23799  trfil2  23823  filssufilg  23847  hausflim  23917  fclsnei  23955  fclsfnflim  23963  flimfnfcls  23964  ptcmplem1  23988  clssubg  24045  tgpconncomp  24049  qustgplem  24057  tsmsfbas  24064  utoptop  24171  iducn  24219  cstucnd  24220  isxmetd  24263  isxmet2d  24264  xmettpos  24286  prdsdsf  24304  prdsmet  24307  ressprdsds  24308  imasdsf1olem  24310  imasf1oxmet  24312  imasf1omet  24313  blfvalps  24320  xmetresbl  24374  metss2  24449  comet  24450  stdbdmet  24453  stdbdmopn  24455  methaus  24457  met2ndci  24459  metustfbas  24494  nrmmetd  24511  subgngp  24572  ngptgp  24573  sranlm  24621  nlmvscnlem1  24623  nlmvscn  24624  nrginvrcn  24629  lssnlm  24638  nghmcn  24682  qtopbaslem  24695  reconn  24766  xmetdcn2  24775  metdscn  24794  metnrm  24800  elcncf1di  24837  cncfcdm  24840  mulc1cncf  24847  cncfco  24849  reparphti  24945  reparphtiOLD  24946  isncvsngpd  25100  tcphcph  25187  ipcnlem1  25195  ipcn  25196  iscfil3  25223  bcthlem5  25278  rrxmet  25358  minveclem3  25379  minveclem7  25385  ovolicc2lem4  25471  dyadmbl  25551  volcn  25557  itg1addlem1  25643  itg1addlem2  25648  itg1addlem4  25650  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  dvmptfsum  25929  c1liplem1  25951  dvgt0lem2  25958  ftc1a  25994  ply1domn  26079  ply1divmo  26091  fta1b  26127  ig1peu  26130  coeeu  26180  plydivalg  26257  aaliou2b  26299  ulmss  26356  ulmcn  26358  efif1olem4  26504  efsubm  26510  logccv  26622  logbmpt  26748  logbfval  26750  cvxcl  26945  basellem4  27044  fsumdvdscom  27145  musum  27151  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dvdsmulf1o  27156  fsumdvdsmulOLD  27157  dchrelbasd  27200  dchrmulcl  27210  dchrinv  27222  lgsqrlem2  27308  lgsdchr  27316  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  2sqreulem4  27415  dchrisumlema  27449  dchrisumlem2  27451  chpdifbndlem2  27515  pntpbnd  27549  pntibndlem3  27553  ssltd  27753  oldbday  27856  addsprop  27926  mulscutlem  28074  divsmo  28127  om2noseqf1o  28224  om2noseqiso  28225  axtgcont  28394  tgjustc1  28400  tgjustc2  28401  iscgrglt  28439  ercgrg  28442  idmot  28462  motco  28465  cnvmot  28466  motcgrg  28469  tgisline  28552  tghilberti2  28563  mirreu3  28579  mirmot  28600  ragperp  28642  foot  28647  mideu  28663  midf  28701  lmimot  28723  trgcopyeu  28731  f1otrgds  28794  f1otrg  28796  f1otrge  28797  xmstrkgc  28811  brbtwn2  28830  axlowdimlem15  28881  axcontlem2  28890  axcontlem10  28898  eengtrkg  28911  eengtrkge  28912  numedglnl  29069  usgredgreu  29143  uspgredg2vtxeu  29145  uspgredg2v  29149  usgredg2v  29152  wlkswwlksf1o  29807  wwlksnextinj  29827  clwlkclwwlkf1  29937  clwwlkf1  29976  frcond4  30197  frgrncvvdeqlem8  30233  frgrncvvdeq  30236  frgrwopreglem4  30242  numclwwlk1lem2f1  30284  nrt2irr  30400  grpoinvf  30459  nvmf  30572  vacn  30621  nmcvcn  30622  smcnlem  30624  sspg  30655  ssps  30657  sspmlem  30659  0lno  30717  blocni  30732  ipblnfi  30782  minvecolem7  30810  unopf1o  31843  cnvunop  31845  unoplin  31847  counop  31848  hmopadj2  31868  hmoplin  31869  bralnfn  31875  lnopeq0i  31934  hmops  31947  hmopm  31948  hmopco  31950  lnconi  31960  cnlnadjlem2  31995  adjmul  32019  adjadd  32020  cdjreui  32359  disjxpin  32515  off2  32565  2ndresdju  32573  fnpreimac  32595  suppovss  32604  f1od2  32644  xrofsup  32690  s3f1  32868  ccatf1  32870  swrdf1  32878  odutos  32894  dfmgc2lem  32921  dfmgc2  32922  pwrssmgc  32926  mgcf1o  32929  mndlactf1  32967  mndractf1  32969  abliso  32977  symgcntz  33042  tocyccntz  33101  archiabllem1  33137  archiabllem2  33141  urpropd  33173  elrgspnlem2  33184  rlocf1  33214  rrgsubm  33224  subrdom  33225  suborng  33283  xrge0slmod  33309  nsgmgc  33373  intlidl  33381  idlinsubrg  33392  rhmimaidl  33393  prmidl2  33402  idlmulssprm  33403  isprmidlc  33408  rhmpreimaprmidl  33412  qsidomlem1  33413  qsidomlem2  33414  ssdifidllem  33417  ssdifidlprm  33419  mxidlprm  33431  mxidlirredi  33432  ssmxidllem  33434  rsprprmprmidl  33483  rsprprmprmidlb  33484  rprmirred  33492  rprmirredb  33493  1arithufdlem4  33508  ply1degltdimlem  33608  ply1degltdim  33609  lindsun  33611  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  lactlmhm  33620  assalactf1o  33621  minplyirred  33691  constrsdrg  33755  1smat1  33781  submateq  33786  madjusmdetlem3  33806  zart0  33856  pstmxmet  33874  ofcf  34080  ldgenpisys  34143  rossros  34157  inelcarsg  34289  sibfof  34318  sitmf  34330  hgt750lemb  34634  erdszelem4  35162  erdszelem9  35167  erdsze2lem2  35172  cnpconn  35198  pconnconn  35199  txpconn  35200  ptpconn  35201  cvxpconn  35210  cvxsconn  35211  iccllysconn  35218  cvmseu  35244  cvmliftmo  35252  cvmlift2lem5  35275  cvmlift2lem9  35279  mrsubff1  35482  elmrsubrn  35488  mrsubco  35489  msubff1  35524  mvhf1  35527  r1peuqusdeg1  35611  segconeu  35975  fnessref  36321  neibastop1  36323  filnetlem3  36344  onsuct0  36405  weiunlem2  36427  unblimceq0lem  36470  unbdqndv2  36475  knoppndv  36498  irrdiff  37290  uncf  37569  fin2so  37577  lindsadd  37583  poimirlem4  37594  poimirlem13  37603  poimirlem14  37604  poimirlem26  37616  heicant  37625  mblfinlem2  37628  ftc1anc  37671  sdclem1  37713  isbnd3  37754  prdsbnd  37763  ismtycnv  37772  ismtyhmeolem  37774  ismtyres  37778  bfplem1  37792  bfplem2  37793  bfp  37794  rrnmet  37799  ismrer1  37808  iccbnd  37810  grpokerinj  37863  isdrngo2  37928  rngogrphom  37941  rngohomco  37944  rngoisocnv  37951  iscringd  37968  eqvreldisj1  38788  erprt  38837  lfl0f  39033  lkrlss  39059  lshpsmreu  39073  linepsubN  39717  pmapsub  39733  lautcnv  40055  lautco  40062  idltrn  40115  cdleme50f1  40508  cdleme50laut  40512  istendod  40727  dihf11  41232  dih1dimatlem  41294  lcfl7N  41466  lcfrlem9  41515  mapd1o  41613  hdmapf1oN  41830  hgmapf1oN  41868  fmpocos  42232  qsalrel  42238  imacrhmcl  42484  evlselv  42557  fsuppind  42560  nacsfix  42682  rmxypairf1o  42882  wepwsolem  43013  dnnumch3  43018  fnwe2  43024  mpaaeu  43121  idomsubgmo  43164  mon1psubm  43170  deg1mhm  43171  isotone1  44019  isotone2  44020  mnringmulrcld  44200  traxext  44950  disjxp1  45041  disjf1  45155  wessf1ornlem  45157  projf1o  45169  sumnnodd  45607  lptioo2  45608  lptioo1  45609  cncfshift  45851  cncfperiod  45856  dvnprodlem1  45923  fourierdlem42  46126  nnfoctbdjlem  46432  isomennd  46508  smflimlem6  46753  fsetsnf1  47029  cfsetsnfsetf1  47036  otiunsndisjX  47256  imasetpreimafvbijlemf1  47366  iccpartgt  47389  icceuelpart  47398  ichnreuop  47434  sprsymrelfolem2  47455  sprsymrelf  47457  prproropf1o  47469  reupr  47484  reuopreuprim  47488  uhgrimprop  47853  isuspgrim0lem  47854  upgrimtrls  47867  gpgprismgr4cycllem11  48052  opmpoismgm  48090  mgmplusgiopALT  48117  2zlidl  48163  rhmsubcALTV  48208  srhmsubcALTV  48248  fldhmsubcALTV  48256  lindslinindsimp1  48381  1arymaptf1  48570  2arymaptf1  48581  fmpodg  48792  toslat  48904  catprsc  48936  catprsc2  48937  oppcendc  48941  invfn  48948  iinfssclem2  48970  iinfssc  48972  iinfsubc  48973  discsubc  48979  nelsubclem  48982  resccatlem  48988  funchomf  49005  imasubclem2  49012  imaidfu  49017  imasubc  49039  imassc  49041  imasubc3  49044  fthcomf  49045  idfth  49046  upeu2  49055  isnatd  49091  swapfffth  49148  diag1f1  49166  diag2f1  49168  isthincd  49270  isthincd2  49271  oppcthinco  49273  oppcthinendcALT  49275  functhinclem4  49281  functhincfun  49283  thincfth  49286  thincciso  49287  thinccisod  49288  functermc  49341  arweuthinc  49362  arweutermc  49363  diagffth  49371