Theorem ralrimivva 3176

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  disjord  5082  disjxiun  5090  otsndisj  5462  otiunsndisj  5463  swopo  5538  issod  5562  reuop  6245  fcof1  7227  fliftfund  7253  isof1oidb  7264  isof1oopb  7265  soisores  7267  soisoi  7268  isocnv  7270  f1oiso  7291  oveqrspc2v  7379  oprres  7520  caovclg  7544  caovcomg  7547  off  7634  coof  7640  caofidlcan  7654  caofrss  7655  caonncan  7660  dmmpog  8012  fnmpoovd  8023  fmpoco  8031  fsplitfpar  8054  poxp  8064  fvmpocurryd  8207  smo11  8290  smoiso2  8295  omsmo  8579  nnasmo  8584  coflton  8592  qsdisj2  8725  eroprf  8745  dom2lem  8921  omxpenlem  8998  xpf1o  9059  unxpdomlem3  9149  fofinf1o  9223  dffi3  9322  supmo  9343  infmo  9388  inf3lem6  9530  cantnf  9590  rankxplim  9779  fseqenlem1  9922  fodomacn  9954  iunfictbso  10012  cofsmo  10167  infpssrlem5  10205  enfin2i  10219  fin23lem23  10224  fin23lem27  10226  fin23lem28  10238  compssiso  10272  ltordlem  11649  cju  12128  axdc4uzlem  13892  seqcaopr2  13947  seqhomo  13958  wrd2ind  14632  cshf1  14719  s3sndisj  14876  s3iunsndisj  14877  climcn2  15502  addcn2  15503  mulcn2  15505  o1of2  15522  isercolllem1  15574  fsum2dlem  15679  fsumcom2  15683  fprodser  15858  fprod2dlem  15889  fprodcom2  15893  isprm6  16627  crth  16691  eulerthlem2  16695  vdwlem12  16906  cshwsdisj  17012  imasaddfnlem  17434  imasvscafn  17443  mreexexd  17556  iscatd  17581  oppccomfpropd  17635  isofn  17684  sectmon  17691  ssctr  17734  ssceq  17735  catsubcat  17748  issubc3  17758  fullsubc  17759  fullresc  17760  isfuncd  17774  idfucl  17790  cofucl  17797  funcres2b  17806  fulloppc  17833  fthoppc  17834  idffth  17844  cofull  17845  cofth  17846  ressffth  17849  setcmon  17996  setcepi  17997  resssetc  18001  resscatc  18018  catciso  18020  fthestrcsetc  18058  fullestrcsetc  18059  embedsetcestrclem  18065  fthsetcestrc  18073  fullsetcestrc  18074  evlfcl  18130  uncfcurf  18147  hofcl  18167  yonedalem3  18188  yonedainv  18189  yonffthlem  18190  yoniso  18193  isdrs2  18214  isposd  18230  pospropd  18233  poslubmo  18317  posglbmo  18318  chnpof1  18538  mgmplusf  18560  ismgmd  18562  issstrmgm  18563  opifismgm  18569  mgmhmpropd  18608  mgmhmf1o  18610  idmgmhm  18611  issubmgm2  18613  rabsubmgmd  18614  resmgmhm  18621  resmgmhm2  18622  resmgmhm2b  18623  mgmhmco  18624  submgmacs  18627  issgrpd  18640  sgrppropd  18641  ismndd  18666  mndpropd  18669  issubmnd  18671  mndinvmod  18674  ismhmd  18696  mhmpropd  18702  idmhm  18705  mhmf1o  18706  issubmd  18716  mndissubm  18717  0mhm  18729  resmhm  18730  resmhm2  18731  resmhm2b  18732  mhmco  18733  submacs  18737  prdspjmhm  18739  pwsdiagmhm  18741  pwsco1mhm  18742  pwsco2mhm  18743  gsumwspan  18756  frmdsssubm  18771  frmdup1  18774  grpsubf  18934  dfgrp3  18954  mhmmnd  18979  mhmfmhm  18980  issubg4  19060  grpissubg  19061  isnsg3  19074  nsgacs  19076  0nsg  19083  nsgid  19084  qus0subgadd  19113  cycsubmcom  19118  isghmd  19139  ghmmhm  19140  idghm  19145  ghmnsgima  19154  ghmnsgpreima  19155  ghmf1  19160  kerf1ghm  19161  ghmf1o  19162  gaid  19213  subgga  19214  gass  19215  gasubg  19216  cntzsgrpcl  19248  cntzsubm  19252  cntrsubgnsg  19257  lactghmga  19319  symgfixf1  19351  odf1  19476  sylow1lem2  19513  sylow2blem2  19535  sylow3lem1  19541  lsmssv  19557  smndlsmidm  19570  pj1eu  19610  efglem  19630  efgtf  19636  efgred  19662  efgredeu  19666  frgpmhm  19679  frgpuptf  19684  frgpuplem  19686  mulgmhm  19741  ghmcmn  19745  invghm  19747  ablnsg  19761  imasabl  19790  cygabl  19805  gsum2d2lem  19887  gsum2d2  19888  gsumcom2  19889  dprd2d2  19960  ablfaclem2  20002  srgfcl  20116  srgcom4lem  20133  srglmhm  20141  srgrmhm  20142  ringcomlem  20199  isrnghm2d  20370  c0mgm  20379  c0mhm  20380  isrhm2d  20406  subrngringnsg  20470  issubrng2  20475  subrngint  20477  issubrg2  20509  subrgint  20512  rnghmsscmap2  20546  rnghmsscmap  20547  rnghmsubcsetclem2  20549  rhmsscmap2  20575  rhmsscmap  20576  rhmsubcsetclem2  20578  rhmsscrnghm  20582  rhmsubcrngclem2  20584  srhmsubc  20597  rhmsubc  20606  fldhmsubc  20702  primefld  20722  abvn0b  20753  suborng  20793  islmodd  20801  lmodscaf  20819  lmodprop2d  20859  islssd  20870  islss4  20897  lssacs  20902  lsspropd  20953  islmhmd  20975  lmhmima  20983  lmhmpreima  20984  reslmhm  20988  lspextmo  20992  lsmcl  21019  pj1lmhm  21036  islbs2  21093  issubrgd  21125  dflidl2rng  21157  rnglidlmmgm  21184  rhmpreimaidl  21216  rngqiprnglin  21241  expmhm  21375  nn0srg  21376  prmirredlem  21411  expghm  21414  mulgghm2  21415  domnchr  21471  znf1o  21490  zntoslem  21495  znfld  21499  cygznlem3  21508  phlipf  21591  dsmmlss  21683  uvcf1  21731  frlmlbs  21736  lindff1  21759  lindfrn  21760  f1lindf  21761  issubassa2  21831  mvrf1  21924  mplsubglem  21937  mplsubrg  21943  mplcoe5lem  21975  mplcoe2  21977  mplind  22006  evlslem2  22015  evlseu  22019  mhplss  22071  ply1sclf1  22204  evls1maplmhm  22293  mamucl  22317  mamuass  22318  mamudi  22319  mamudir  22320  mamuvs1  22321  mamuvs2  22322  matbas2d  22339  mamumat1cl  22355  mamulid  22357  mamurid  22358  mat1mhm  22400  dmatid  22411  dmatsubcl  22414  dmatsgrp  22415  dmatmulcl  22416  dmatsrng  22417  dmatcrng  22418  scmatscmiddistr  22424  scmatscm  22429  scmatsgrp  22435  scmatsrng  22436  scmatcrng  22437  scmatsgrp1  22438  scmatsrng1  22439  scmatf1  22447  scmatmhm  22450  mavmul0g  22469  mdet1  22517  mdetunilem9  22536  mdetuni0  22537  mdetmul  22539  madutpos  22558  smadiadetlem4  22585  1elcpmat  22631  cpmatacl  22632  cpmatmcl  22635  mat2pmatf1  22645  mat2pmatmul  22647  mat2pmat1  22648  mat2pmatlin  22651  m2cpm  22657  m2cpminvid  22669  m2cpminvid2  22671  decpmatmul  22688  pmatcollpw1  22692  monmatcollpw  22695  pmatcollpw  22697  pmatcollpw3lem  22699  pmatcollpwscmatlem2  22706  pm2mpf1  22715  mp2pm2mplem4  22725  pm2mpmhmlem2  22735  chp0mat  22762  chpidmat  22763  tgclb  22886  mretopd  23008  toponmre  23009  iscldtop  23011  ordtbaslem  23104  ordtbas2  23107  cnt0  23262  haust1  23268  cnhaus  23270  isreg2  23293  dishaus  23298  ordthaus  23300  dfconn2  23335  iunconn  23344  clsconn  23346  2ndcomap  23374  dis2ndc  23376  llynlly  23393  restnlly  23398  restlly  23399  islly2  23400  llyidm  23404  nllyidm  23405  hausllycmp  23410  kgentopon  23454  txbas  23483  ptbasin2  23494  ptbasfi  23497  txcnp  23536  txcnmpt  23540  pthaus  23554  tx1stc  23566  xkococnlem  23575  xkococn  23576  cnmpt21  23587  qtoptop2  23615  qtopeu  23632  kqt0lem  23652  isr0  23653  regr1lem2  23656  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  nrmr0reg  23665  reghmph  23709  nrmhmph  23710  txswaphmeo  23721  qtophmeo  23733  fbun  23756  trfbas2  23759  isfil2  23772  infil  23779  trfil2  23803  filssufilg  23827  hausflim  23897  fclsnei  23935  fclsfnflim  23943  flimfnfcls  23944  ptcmplem1  23968  clssubg  24025  tgpconncomp  24029  qustgplem  24037  tsmsfbas  24044  utoptop  24150  iducn  24198  cstucnd  24199  isxmetd  24242  isxmet2d  24243  xmettpos  24265  prdsdsf  24283  prdsmet  24286  ressprdsds  24287  imasdsf1olem  24289  imasf1oxmet  24291  imasf1omet  24292  blfvalps  24299  xmetresbl  24353  metss2  24428  comet  24429  stdbdmet  24432  stdbdmopn  24434  methaus  24436  met2ndci  24438  metustfbas  24473  nrmmetd  24490  subgngp  24551  ngptgp  24552  sranlm  24600  nlmvscnlem1  24602  nlmvscn  24603  nrginvrcn  24608  lssnlm  24617  nghmcn  24661  qtopbaslem  24674  reconn  24745  xmetdcn2  24754  metdscn  24773  metnrm  24779  elcncf1di  24816  cncfcdm  24819  mulc1cncf  24826  cncfco  24828  reparphti  24924  reparphtiOLD  24925  isncvsngpd  25078  tcphcph  25165  ipcnlem1  25173  ipcn  25174  iscfil3  25201  bcthlem5  25256  rrxmet  25336  minveclem3  25357  minveclem7  25363  ovolicc2lem4  25449  dyadmbl  25529  volcn  25535  itg1addlem1  25621  itg1addlem2  25626  itg1addlem4  25628  mbfi1fseqlem1  25644  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  dvmptfsum  25907  c1liplem1  25929  dvgt0lem2  25936  ftc1a  25972  ply1domn  26057  ply1divmo  26069  fta1b  26105  ig1peu  26108  coeeu  26158  plydivalg  26235  aaliou2b  26277  ulmss  26334  ulmcn  26336  efif1olem4  26482  efsubm  26488  logccv  26600  logbmpt  26726  logbfval  26728  cvxcl  26923  basellem4  27022  fsumdvdscom  27123  musum  27129  mpodvdsmulf1o  27132  fsumdvdsmul  27133  dvdsmulf1o  27134  fsumdvdsmulOLD  27135  dchrelbasd  27178  dchrmulcl  27188  dchrinv  27200  lgsqrlem2  27286  lgsdchr  27294  lgseisenlem2  27315  lgsquadlem1  27319  lgsquadlem2  27320  2sqreulem4  27393  dchrisumlema  27427  dchrisumlem2  27429  chpdifbndlem2  27493  pntpbnd  27527  pntibndlem3  27531  ssltd  27732  oldbday  27847  addsprop  27920  mulscutlem  28071  divsmo  28124  om2noseqf1o  28232  om2noseqiso  28233  axtgcont  28448  tgjustc1  28454  tgjustc2  28455  iscgrglt  28493  ercgrg  28496  idmot  28516  motco  28519  cnvmot  28520  motcgrg  28523  tgisline  28606  tghilberti2  28617  mirreu3  28633  mirmot  28654  ragperp  28696  foot  28701  mideu  28717  midf  28755  lmimot  28777  trgcopyeu  28785  f1otrgds  28848  f1otrg  28850  f1otrge  28851  xmstrkgc  28865  brbtwn2  28885  axlowdimlem15  28936  axcontlem2  28945  axcontlem10  28953  eengtrkg  28966  eengtrkge  28967  numedglnl  29124  usgredgreu  29198  uspgredg2vtxeu  29200  uspgredg2v  29204  usgredg2v  29207  wlkswwlksf1o  29859  wwlksnextinj  29879  clwlkclwwlkf1  29992  clwwlkf1  30031  frcond4  30252  frgrncvvdeqlem8  30288  frgrncvvdeq  30291  frgrwopreglem4  30297  numclwwlk1lem2f1  30339  nrt2irr  30455  grpoinvf  30514  nvmf  30627  vacn  30676  nmcvcn  30677  smcnlem  30679  sspg  30710  ssps  30712  sspmlem  30714  0lno  30772  blocni  30787  ipblnfi  30837  minvecolem7  30865  unopf1o  31898  cnvunop  31900  unoplin  31902  counop  31903  hmopadj2  31923  hmoplin  31924  bralnfn  31930  lnopeq0i  31989  hmops  32002  hmopm  32003  hmopco  32005  lnconi  32015  cnlnadjlem2  32050  adjmul  32074  adjadd  32075  cdjreui  32414  disjxpin  32570  off2  32625  2ndresdju  32633  fnpreimac  32655  suppovss  32666  f1od2  32706  xrofsup  32754  s3f1  32935  ccatf1  32937  swrdf1  32944  odutos  32956  dfmgc2lem  32983  dfmgc2  32984  pwrssmgc  32988  mgcf1o  32991  mndlactf1  33014  mndractf1  33016  abliso  33024  symgcntz  33061  tocyccntz  33120  conjga  33146  fxpsubrg  33150  archiabllem1  33169  archiabllem2  33173  urpropd  33206  elrgspnlem2  33217  rlocf1  33247  rrgsubm  33257  subrdom  33258  xrge0slmod  33320  nsgmgc  33384  intlidl  33392  idlinsubrg  33403  rhmimaidl  33404  prmidl2  33413  idlmulssprm  33414  isprmidlc  33419  rhmpreimaprmidl  33423  qsidomlem1  33424  qsidomlem2  33425  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  mxidlirredi  33443  ssmxidllem  33445  rsprprmprmidl  33494  rsprprmprmidlb  33495  rprmirred  33503  rprmirredb  33504  1arithufdlem4  33519  extvfvcl  33587  mplvrpmga  33593  ply1degltdimlem  33656  ply1degltdim  33657  lindsun  33659  fedgmullem1  33663  fedgmullem2  33664  fedgmul  33665  lactlmhm  33668  assalactf1o  33669  minplyirred  33745  constrsdrg  33809  1smat1  33838  submateq  33843  madjusmdetlem3  33863  zart0  33913  pstmxmet  33931  ofcf  34137  ldgenpisys  34200  rossros  34214  inelcarsg  34345  sibfof  34374  sitmf  34386  hgt750lemb  34690  erdszelem4  35259  erdszelem9  35264  erdsze2lem2  35269  cnpconn  35295  pconnconn  35296  txpconn  35297  ptpconn  35298  cvxpconn  35307  cvxsconn  35308  iccllysconn  35315  cvmseu  35341  cvmliftmo  35349  cvmlift2lem5  35372  cvmlift2lem9  35376  mrsubff1  35579  elmrsubrn  35585  mrsubco  35586  msubff1  35621  mvhf1  35624  r1peuqusdeg1  35708  segconeu  36076  fnessref  36422  neibastop1  36424  filnetlem3  36445  onsuct0  36506  weiunlem2  36528  unblimceq0lem  36571  unbdqndv2  36576  knoppndv  36599  irrdiff  37391  uncf  37659  fin2so  37667  lindsadd  37673  poimirlem4  37684  poimirlem13  37693  poimirlem14  37694  poimirlem26  37706  heicant  37715  mblfinlem2  37718  ftc1anc  37761  sdclem1  37803  isbnd3  37844  prdsbnd  37853  ismtycnv  37862  ismtyhmeolem  37864  ismtyres  37868  bfplem1  37882  bfplem2  37883  bfp  37884  rrnmet  37889  ismrer1  37898  iccbnd  37900  grpokerinj  37953  isdrngo2  38018  rngogrphom  38031  rngohomco  38034  rngoisocnv  38041  iscringd  38058  eqvreldisj1  38942  erprt  38992  lfl0f  39188  lkrlss  39214  lshpsmreu  39228  linepsubN  39871  pmapsub  39887  lautcnv  40209  lautco  40216  idltrn  40269  cdleme50f1  40662  cdleme50laut  40666  istendod  40881  dihf11  41386  dih1dimatlem  41448  lcfl7N  41620  lcfrlem9  41669  mapd1o  41767  hdmapf1oN  41984  hgmapf1oN  42022  fmpocos  42352  qsalrel  42358  rediveud  42561  imacrhmcl  42632  evlselv  42705  fsuppind  42708  nacsfix  42829  rmxypairf1o  43028  wepwsolem  43159  dnnumch3  43164  fnwe2  43170  mpaaeu  43267  idomsubgmo  43310  mon1psubm  43316  deg1mhm  43317  isotone1  44165  isotone2  44166  mnringmulrcld  44345  traxext  45094  disjxp1  45190  disjf1  45304  wessf1ornlem  45306  projf1o  45318  sumnnodd  45754  lptioo2  45755  lptioo1  45756  cncfshift  45996  cncfperiod  46001  dvnprodlem1  46068  fourierdlem42  46271  nnfoctbdjlem  46577  isomennd  46653  smflimlem6  46898  fsetsnf1  47176  cfsetsnfsetf1  47183  otiunsndisjX  47403  imasetpreimafvbijlemf1  47528  iccpartgt  47551  icceuelpart  47560  ichnreuop  47596  sprsymrelfolem2  47617  sprsymrelf  47619  prproropf1o  47631  reupr  47646  reuopreuprim  47650  uhgrimprop  48016  isuspgrim0lem  48017  upgrimtrls  48030  gpgprismgr4cycllem11  48229  opmpoismgm  48291  mgmplusgiopALT  48318  2zlidl  48364  rhmsubcALTV  48409  srhmsubcALTV  48449  fldhmsubcALTV  48457  lindslinindsimp1  48582  1arymaptf1  48767  2arymaptf1  48778  eqfnovd  48990  fmpodg  48993  toslat  49106  catprsc  49138  catprsc2  49139  oppcendc  49143  invfn  49155  iinfssclem2  49180  iinfssc  49182  iinfsubc  49183  discsubc  49189  nelsubclem  49192  resccatlem  49198  funchomf  49222  imasubclem2  49230  imaidfu  49235  imasubc  49276  imassc  49278  imasubc3  49281  fthcomf  49282  idfth  49283  cofidfth  49287  upeu2  49297  isnatd  49348  swapfffth  49408  diag1f1  49432  diag2f1  49434  fucoppc  49535  isthincd  49561  isthincd2  49562  oppcthinco  49564  oppcthinendcALT  49566  functhinclem4  49572  functhincfun  49574  thincfth  49577  thincciso  49578  thinccisod  49579  functermc  49633  arweuthinc  49654  arweutermc  49655  diagffth  49663  funcsn  49666  0fucterm  49668