Theorem ralrimivva 3202

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

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

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 3062

This theorem is referenced by:  disjord  5132  disjxiun  5140  otsndisj  5524  otiunsndisj  5525  swopo  5603  issod  5627  reuop  6313  fcof1  7307  fliftfund  7333  isof1oidb  7344  isof1oopb  7345  soisores  7347  soisoi  7348  isocnv  7350  f1oiso  7371  oveqrspc2v  7458  oprres  7601  caovclg  7625  caovcomg  7628  off  7715  coof  7721  caofidlcan  7735  caofrss  7736  caonncan  7741  dmmpog  8099  fnmpoovd  8112  fmpoco  8120  fsplitfpar  8143  poxp  8153  fvmpocurryd  8296  smo11  8404  smoiso2  8409  omsmo  8696  nnasmo  8701  coflton  8709  qsdisj2  8835  eroprf  8855  dom2lem  9032  omxpenlem  9113  xpf1o  9179  unxpdomlem3  9288  fofinf1o  9372  dffi3  9471  supmo  9492  infmo  9535  inf3lem6  9673  cantnf  9733  rankxplim  9919  fseqenlem1  10064  fodomacn  10096  iunfictbso  10154  cofsmo  10309  infpssrlem5  10347  enfin2i  10361  fin23lem23  10366  fin23lem27  10368  fin23lem28  10380  compssiso  10414  ltordlem  11788  cju  12262  axdc4uzlem  14024  seqcaopr2  14079  seqhomo  14090  wrd2ind  14761  cshf1  14848  s3sndisj  15006  s3iunsndisj  15007  climcn2  15629  addcn2  15630  mulcn2  15632  o1of2  15649  isercolllem1  15701  fsum2dlem  15806  fsumcom2  15810  fprodser  15985  fprod2dlem  16016  fprodcom2  16020  isprm6  16751  crth  16815  eulerthlem2  16819  vdwlem12  17030  cshwsdisj  17136  imasaddfnlem  17573  imasvscafn  17582  mreexexd  17691  iscatd  17716  oppccomfpropd  17770  isofn  17819  sectmon  17826  ssctr  17869  ssceq  17870  catsubcat  17884  issubc3  17894  fullsubc  17895  fullresc  17896  isfuncd  17910  idfucl  17926  cofucl  17933  funcres2b  17942  fulloppc  17969  fthoppc  17970  idffth  17980  cofull  17981  cofth  17982  ressffth  17985  setcmon  18132  setcepi  18133  resssetc  18137  resscatc  18154  catciso  18156  fthestrcsetc  18195  fullestrcsetc  18196  embedsetcestrclem  18202  fthsetcestrc  18210  fullsetcestrc  18211  evlfcl  18267  uncfcurf  18284  hofcl  18304  yonedalem3  18325  yonedainv  18326  yonffthlem  18327  yoniso  18330  isdrs2  18352  isposd  18368  pospropd  18372  poslubmo  18456  posglbmo  18457  mgmplusf  18663  ismgmd  18665  issstrmgm  18666  opifismgm  18672  mgmhmpropd  18711  mgmhmf1o  18713  idmgmhm  18714  issubmgm2  18716  rabsubmgmd  18717  resmgmhm  18724  resmgmhm2  18725  resmgmhm2b  18726  mgmhmco  18727  submgmacs  18730  issgrpd  18743  sgrppropd  18744  ismndd  18769  mndpropd  18772  issubmnd  18774  mndinvmod  18777  ismhmd  18799  mhmpropd  18805  idmhm  18808  mhmf1o  18809  issubmd  18819  mndissubm  18820  0mhm  18832  resmhm  18833  resmhm2  18834  resmhm2b  18835  mhmco  18836  submacs  18840  prdspjmhm  18842  pwsdiagmhm  18844  pwsco1mhm  18845  pwsco2mhm  18846  gsumwspan  18859  frmdsssubm  18874  frmdup1  18877  grpsubf  19037  dfgrp3  19057  mhmmnd  19082  mhmfmhm  19083  issubg4  19163  grpissubg  19164  isnsg3  19178  nsgacs  19180  0nsg  19187  nsgid  19188  qus0subgadd  19217  cycsubmcom  19222  isghmd  19243  ghmmhm  19244  idghm  19249  ghmnsgima  19258  ghmnsgpreima  19259  ghmf1  19264  kerf1ghm  19265  ghmf1o  19266  gaid  19317  subgga  19318  gass  19319  gasubg  19320  cntzsgrpcl  19352  cntzsubm  19356  cntrsubgnsg  19361  lactghmga  19423  symgfixf1  19455  odf1  19580  sylow1lem2  19617  sylow2blem2  19639  sylow3lem1  19645  lsmssv  19661  smndlsmidm  19674  pj1eu  19714  efglem  19734  efgtf  19740  efgred  19766  efgredeu  19770  frgpmhm  19783  frgpuptf  19788  frgpuplem  19790  mulgmhm  19845  ghmcmn  19849  invghm  19851  ablnsg  19865  imasabl  19894  cygabl  19909  gsum2d2lem  19991  gsum2d2  19992  gsumcom2  19993  dprd2d2  20064  ablfaclem2  20106  srgfcl  20193  srgcom4lem  20210  srglmhm  20218  srgrmhm  20219  ringcomlem  20276  isrnghm2d  20450  c0mgm  20459  c0mhm  20460  isrhm2d  20487  subrngringnsg  20553  issubrng2  20558  subrngint  20560  issubrg2  20592  subrgint  20595  rnghmsscmap2  20629  rnghmsscmap  20630  rnghmsubcsetclem2  20632  rhmsscmap2  20658  rhmsscmap  20659  rhmsubcsetclem2  20661  rhmsscrnghm  20665  rhmsubcrngclem2  20667  srhmsubc  20680  rhmsubc  20689  fldhmsubc  20786  primefld  20806  abvn0b  20837  islmodd  20864  lmodscaf  20882  lmodprop2d  20922  islssd  20933  islss4  20960  lssacs  20965  lsspropd  21016  islmhmd  21038  lmhmima  21046  lmhmpreima  21047  reslmhm  21051  lspextmo  21055  lsmcl  21082  pj1lmhm  21099  islbs2  21156  issubrgd  21196  dflidl2rng  21228  rnglidlmmgm  21255  rhmpreimaidl  21287  rngqiprnglin  21312  expmhm  21454  nn0srg  21455  prmirredlem  21483  expghm  21486  mulgghm2  21487  domnchr  21547  znf1o  21570  zntoslem  21575  znfld  21579  cygznlem3  21588  phlipf  21670  dsmmlss  21764  uvcf1  21812  frlmlbs  21817  lindff1  21840  lindfrn  21841  f1lindf  21842  issubassa2  21912  mvrf1  22006  mplsubglem  22019  mplsubrg  22025  mplcoe5lem  22057  mplcoe2  22059  mplind  22094  evlslem2  22103  evlseu  22107  mhplss  22159  ply1sclf1  22292  evls1maplmhm  22381  mamucl  22405  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  matbas2d  22429  mamumat1cl  22445  mamulid  22447  mamurid  22448  mat1mhm  22490  dmatid  22501  dmatsubcl  22504  dmatsgrp  22505  dmatmulcl  22506  dmatsrng  22507  dmatcrng  22508  scmatscmiddistr  22514  scmatscm  22519  scmatsgrp  22525  scmatsrng  22526  scmatcrng  22527  scmatsgrp1  22528  scmatsrng1  22529  scmatf1  22537  scmatmhm  22540  mavmul0g  22559  mdet1  22607  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  madutpos  22648  smadiadetlem4  22675  1elcpmat  22721  cpmatacl  22722  cpmatmcl  22725  mat2pmatf1  22735  mat2pmatmul  22737  mat2pmat1  22738  mat2pmatlin  22741  m2cpm  22747  m2cpminvid  22759  m2cpminvid2  22761  decpmatmul  22778  pmatcollpw1  22782  monmatcollpw  22785  pmatcollpw  22787  pmatcollpw3lem  22789  pmatcollpwscmatlem2  22796  pm2mpf1  22805  mp2pm2mplem4  22815  pm2mpmhmlem2  22825  chp0mat  22852  chpidmat  22853  tgclb  22977  mretopd  23100  toponmre  23101  iscldtop  23103  ordtbaslem  23196  ordtbas2  23199  cnt0  23354  haust1  23360  cnhaus  23362  isreg2  23385  dishaus  23390  ordthaus  23392  dfconn2  23427  iunconn  23436  clsconn  23438  2ndcomap  23466  dis2ndc  23468  llynlly  23485  restnlly  23490  restlly  23491  islly2  23492  llyidm  23496  nllyidm  23497  hausllycmp  23502  kgentopon  23546  txbas  23575  ptbasin2  23586  ptbasfi  23589  txcnp  23628  txcnmpt  23632  pthaus  23646  tx1stc  23658  xkococnlem  23667  xkococn  23668  cnmpt21  23679  qtoptop2  23707  qtopeu  23724  kqt0lem  23744  isr0  23745  regr1lem2  23748  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  nrmr0reg  23757  reghmph  23801  nrmhmph  23802  txswaphmeo  23813  qtophmeo  23825  fbun  23848  trfbas2  23851  isfil2  23864  infil  23871  trfil2  23895  filssufilg  23919  hausflim  23989  fclsnei  24027  fclsfnflim  24035  flimfnfcls  24036  ptcmplem1  24060  clssubg  24117  tgpconncomp  24121  qustgplem  24129  tsmsfbas  24136  utoptop  24243  iducn  24292  cstucnd  24293  isxmetd  24336  isxmet2d  24337  xmettpos  24359  prdsdsf  24377  prdsmet  24380  ressprdsds  24381  imasdsf1olem  24383  imasf1oxmet  24385  imasf1omet  24386  blfvalps  24393  xmetresbl  24447  metss2  24525  comet  24526  stdbdmet  24529  stdbdmopn  24531  methaus  24533  met2ndci  24535  metustfbas  24570  nrmmetd  24587  subgngp  24648  ngptgp  24649  sranlm  24705  nlmvscnlem1  24707  nlmvscn  24708  nrginvrcn  24713  lssnlm  24722  nghmcn  24766  qtopbaslem  24779  reconn  24850  xmetdcn2  24859  metdscn  24878  metnrm  24884  elcncf1di  24921  cncfcdm  24924  mulc1cncf  24931  cncfco  24933  reparphti  25029  reparphtiOLD  25030  isncvsngpd  25184  tcphcph  25271  ipcnlem1  25279  ipcn  25280  iscfil3  25307  bcthlem5  25362  rrxmet  25442  minveclem3  25463  minveclem7  25469  ovolicc2lem4  25555  dyadmbl  25635  volcn  25641  itg1addlem1  25727  itg1addlem2  25732  itg1addlem4  25734  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  dvmptfsum  26013  c1liplem1  26035  dvgt0lem2  26042  ftc1a  26078  ply1domn  26163  ply1divmo  26175  fta1b  26211  ig1peu  26214  coeeu  26264  plydivalg  26341  aaliou2b  26383  ulmss  26440  ulmcn  26442  efif1olem4  26587  efsubm  26593  logccv  26705  logbmpt  26831  logbfval  26833  cvxcl  27028  basellem4  27127  fsumdvdscom  27228  musum  27234  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  dchrelbasd  27283  dchrmulcl  27293  dchrinv  27305  lgsqrlem2  27391  lgsdchr  27399  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  2sqreulem4  27498  dchrisumlema  27532  dchrisumlem2  27534  chpdifbndlem2  27598  pntpbnd  27632  pntibndlem3  27636  ssltd  27836  oldbday  27939  addsprop  28009  mulscutlem  28157  divsmo  28210  om2noseqf1o  28307  om2noseqiso  28308  axtgcont  28477  tgjustc1  28483  tgjustc2  28484  iscgrglt  28522  ercgrg  28525  idmot  28545  motco  28548  cnvmot  28549  motcgrg  28552  tgisline  28635  tghilberti2  28646  mirreu3  28662  mirmot  28683  ragperp  28725  foot  28730  mideu  28746  midf  28784  lmimot  28806  trgcopyeu  28814  f1otrgds  28877  f1otrg  28879  f1otrge  28880  xmstrkgc  28900  brbtwn2  28920  axlowdimlem15  28971  axcontlem2  28980  axcontlem10  28988  eengtrkg  29001  eengtrkge  29002  numedglnl  29161  usgredgreu  29235  uspgredg2vtxeu  29237  uspgredg2v  29241  usgredg2v  29244  wlkswwlksf1o  29899  wwlksnextinj  29919  clwlkclwwlkf1  30029  clwwlkf1  30068  frcond4  30289  frgrncvvdeqlem8  30325  frgrncvvdeq  30328  frgrwopreglem4  30334  numclwwlk1lem2f1  30376  nrt2irr  30492  grpoinvf  30551  nvmf  30664  vacn  30713  nmcvcn  30714  smcnlem  30716  sspg  30747  ssps  30749  sspmlem  30751  0lno  30809  blocni  30824  ipblnfi  30874  minvecolem7  30902  unopf1o  31935  cnvunop  31937  unoplin  31939  counop  31940  hmopadj2  31960  hmoplin  31961  bralnfn  31967  lnopeq0i  32026  hmops  32039  hmopm  32040  hmopco  32042  lnconi  32052  cnlnadjlem2  32087  adjmul  32111  adjadd  32112  cdjreui  32451  disjxpin  32601  off2  32651  2ndresdju  32659  fnpreimac  32681  suppovss  32690  f1od2  32732  xrofsup  32771  s3f1  32931  ccatf1  32933  swrdf1  32941  odutos  32958  dfmgc2lem  32985  dfmgc2  32986  pwrssmgc  32990  mgcf1o  32993  mndlactf1  33031  mndractf1  33033  abliso  33041  symgcntz  33105  tocyccntz  33164  archiabllem1  33200  archiabllem2  33204  urpropd  33236  elrgspnlem2  33247  rlocf1  33277  rrgsubm  33287  subrdom  33288  suborng  33345  xrge0slmod  33376  nsgmgc  33440  intlidl  33448  idlinsubrg  33459  rhmimaidl  33460  prmidl2  33469  idlmulssprm  33470  isprmidlc  33475  rhmpreimaprmidl  33479  qsidomlem1  33480  qsidomlem2  33481  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  ssmxidllem  33501  rsprprmprmidl  33550  rsprprmprmidlb  33551  rprmirred  33559  rprmirredb  33560  1arithufdlem4  33575  ply1degltdimlem  33673  ply1degltdim  33674  lindsun  33676  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  lactlmhm  33685  assalactf1o  33686  minplyirred  33754  1smat1  33803  submateq  33808  madjusmdetlem3  33828  zart0  33878  pstmxmet  33896  ofcf  34104  ldgenpisys  34167  rossros  34181  inelcarsg  34313  sibfof  34342  sitmf  34354  hgt750lemb  34671  erdszelem4  35199  erdszelem9  35204  erdsze2lem2  35209  cnpconn  35235  pconnconn  35236  txpconn  35237  ptpconn  35238  cvxpconn  35247  cvxsconn  35248  iccllysconn  35255  cvmseu  35281  cvmliftmo  35289  cvmlift2lem5  35312  cvmlift2lem9  35316  mrsubff1  35519  elmrsubrn  35525  mrsubco  35526  msubff1  35561  mvhf1  35564  r1peuqusdeg1  35648  segconeu  36012  fnessref  36358  neibastop1  36360  filnetlem3  36381  onsuct0  36442  weiunlem2  36464  unblimceq0lem  36507  unbdqndv2  36512  knoppndv  36535  irrdiff  37327  uncf  37606  fin2so  37614  lindsadd  37620  poimirlem4  37631  poimirlem13  37640  poimirlem14  37641  poimirlem26  37653  heicant  37662  mblfinlem2  37665  ftc1anc  37708  sdclem1  37750  isbnd3  37791  prdsbnd  37800  ismtycnv  37809  ismtyhmeolem  37811  ismtyres  37815  bfplem1  37829  bfplem2  37830  bfp  37831  rrnmet  37836  ismrer1  37845  iccbnd  37847  grpokerinj  37900  isdrngo2  37965  rngogrphom  37978  rngohomco  37981  rngoisocnv  37988  iscringd  38005  eqvreldisj1  38825  erprt  38874  lfl0f  39070  lkrlss  39096  lshpsmreu  39110  linepsubN  39754  pmapsub  39770  lautcnv  40092  lautco  40099  idltrn  40152  cdleme50f1  40545  cdleme50laut  40549  istendod  40764  dihf11  41269  dih1dimatlem  41331  lcfl7N  41503  lcfrlem9  41552  mapd1o  41650  hdmapf1oN  41867  hgmapf1oN  41905  fmpocos  42275  qsalrel  42281  imacrhmcl  42524  evlselv  42597  fsuppind  42600  nacsfix  42723  rmxypairf1o  42923  wepwsolem  43054  dnnumch3  43059  fnwe2  43065  mpaaeu  43162  idomsubgmo  43205  mon1psubm  43211  deg1mhm  43212  isotone1  44061  isotone2  44062  mnringmulrcld  44247  traxext  44994  disjxp1  45074  disjf1  45188  wessf1ornlem  45190  projf1o  45202  sumnnodd  45645  lptioo2  45646  lptioo1  45647  cncfshift  45889  cncfperiod  45894  dvnprodlem1  45961  fourierdlem42  46164  nnfoctbdjlem  46470  isomennd  46546  smflimlem6  46791  fsetsnf1  47064  cfsetsnfsetf1  47071  otiunsndisjX  47291  imasetpreimafvbijlemf1  47391  iccpartgt  47414  icceuelpart  47423  ichnreuop  47459  sprsymrelfolem2  47480  sprsymrelf  47482  prproropf1o  47494  reupr  47509  reuopreuprim  47513  isuspgrim0lem  47871  uspgrimprop  47873  opmpoismgm  48083  mgmplusgiopALT  48110  2zlidl  48156  rhmsubcALTV  48201  srhmsubcALTV  48241  fldhmsubcALTV  48249  lindslinindsimp1  48374  1arymaptf1  48563  2arymaptf1  48574  fmpodg  48769  toslat  48871  catprsc  48902  catprsc2  48903  oppcendc  48906  upeu2  48929  isnatd  48949  swapfffth  48989  isthincd  49085  isthincd2  49086  oppcthinco  49088  oppcthinendcALT  49090  functhinclem4  49096  functhincfun  49098  thincfth  49101  thincciso  49102  thinccisod  49103  functermc  49140