Theorem ralrimivva 3207

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 416	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 3205	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  disjord  5091  disjxiun  5099  otsndisj  5490  otiunsndisj  5491  swopo  5568  issod  5592  reuop  6282  fcof1  7273  fliftfund  7299  isof1oidb  7310  isof1oopb  7311  soisores  7313  soisoi  7314  isocnv  7316  f1oiso  7337  oveqrspc2v  7425  oprres  7566  caovclg  7590  caovcomg  7593  off  7680  coof  7686  caofidlcan  7700  caofrss  7701  caonncan  7706  dmmpog  8057  fnmpoovd  8068  fmpoco  8076  fsplitfpar  8099  poxp  8110  fvmpocurryd  8253  smo11  8337  smoiso2  8342  omsmo  8630  nnasmo  8635  coflton  8643  qsdisj2  8779  eroprf  8799  dom2lem  8975  omxpenlem  9052  xpf1o  9113  unxpdomlem3  9204  fofinf1o  9277  dffi3  9379  supmo  9400  infmo  9445  inf3lem6  9590  cantnf  9650  rankxplim  9839  fseqenlem1  9982  fodomacn  10014  iunfictbso  10072  cofsmo  10228  infpssrlem5  10266  enfin2i  10280  fin23lem23  10285  fin23lem27  10287  fin23lem28  10299  compssiso  10333  ltordlem  11714  cju  12193  axdc4uzlem  13998  seqcaopr2  14053  seqhomo  14064  wrd2ind  14738  cshf1  14825  s3sndisj  14982  s3iunsndisj  14983  climcn2  15622  addcn2  15623  mulcn2  15625  o1of2  15642  isercolllem1  15694  fsum2dlem  15799  fsumcom2  15803  fprodser  15981  fprod2dlem  16012  fprodcom2  16016  isprm6  16751  crth  16815  eulerthlem2  16819  vdwlem12  17030  cshwsdisj  17136  imasaddfnlem  17560  imasvscafn  17569  mreexexd  17682  iscatd  17707  oppccomfpropd  17761  isofn  17810  sectmon  17817  ssctr  17860  ssceq  17861  catsubcat  17874  issubc3  17884  fullsubc  17885  fullresc  17886  isfuncd  17900  idfucl  17916  cofucl  17923  funcres2b  17932  fulloppc  17959  fthoppc  17960  idffth  17970  cofull  17971  cofth  17972  ressffth  17975  setcmon  18122  setcepi  18123  resssetc  18127  resscatc  18144  catciso  18146  fthestrcsetc  18184  fullestrcsetc  18185  embedsetcestrclem  18191  fthsetcestrc  18199  fullsetcestrc  18200  evlfcl  18256  uncfcurf  18273  hofcl  18293  yonedalem3  18314  yonedainv  18315  yonffthlem  18316  yoniso  18319  isdrs2  18340  isposd  18356  pospropd  18359  poslubmo  18443  posglbmo  18444  chnpof1  18664  mgmplusf  18686  ismgmd  18688  issstrmgm  18689  opifismgm  18695  mgmhmpropd  18734  mgmhmf1o  18736  idmgmhm  18737  issubmgm2  18739  rabsubmgmd  18740  resmgmhm  18747  resmgmhm2  18748  resmgmhm2b  18749  mgmhmco  18750  submgmacs  18753  issgrpd  18766  sgrppropd  18767  ismndd  18792  mndpropd  18795  issubmnd  18797  mndinvmod  18800  ismhmd  18822  mhmpropd  18828  idmhm  18831  mhmf1o  18832  issubmd  18842  mndissubm  18843  0mhm  18855  resmhm  18856  resmhm2  18857  resmhm2b  18858  mhmco  18859  submacs  18863  prdspjmhm  18865  pwsdiagmhm  18867  pwsco1mhm  18868  pwsco2mhm  18869  gsumwspan  18882  frmdsssubm  18897  frmdup1  18900  grpsubf  19063  dfgrp3  19083  mhmmnd  19108  mhmfmhm  19109  issubg4  19189  grpissubg  19190  isnsg3  19203  nsgacs  19205  0nsg  19212  nsgid  19213  qus0subgadd  19242  cycsubmcom  19247  isghmd  19267  ghmmhm  19268  idghm  19273  ghmnsgima  19282  ghmnsgpreima  19283  ghmf1  19288  kerf1ghm  19289  ghmf1o  19290  gaid  19341  subgga  19342  gass  19343  gasubg  19344  cntzsgrpcl  19376  cntzsubm  19380  cntrsubgnsg  19385  lactghmga  19447  symgfixf1  19479  odf1  19604  sylow1lem2  19641  sylow2blem2  19663  sylow3lem1  19669  lsmssv  19685  smndlsmidm  19698  pj1eu  19738  efglem  19758  efgtf  19764  efgred  19790  efgredeu  19794  frgpmhm  19807  frgpuptf  19812  frgpuplem  19814  mulgmhm  19869  ghmcmn  19873  invghm  19875  ablnsg  19889  imasabl  19918  cygabl  19933  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  dprd2d2  20088  ablfaclem2  20130  srgfcl  20248  srgcom4lem  20265  srglmhm  20273  srgrmhm  20274  ringcomlem  20331  isrnghm2d  20501  c0mgm  20510  c0mhm  20511  isrhm2d  20538  subrngringnsg  20605  issubrng2  20610  subrngint  20612  issubrg2  20644  subrgint  20647  rnghmsscmap2  20681  rnghmsscmap  20682  rnghmsubcsetclem2  20684  rhmsscmap2  20710  rhmsscmap  20711  rhmsubcsetclem2  20713  rhmsscrnghm  20717  rhmsubcrngclem2  20719  srhmsubc  20732  rhmsubc  20741  fldhmsubc  20836  primefld  20856  abvn0b  20887  suborng  20927  islmodd  20935  lmodscaf  20953  lmodprop2d  20993  islssd  21004  islss4  21031  lssacs  21036  lsspropd  21086  islmhmd  21108  lmhmima  21116  lmhmpreima  21117  reslmhm  21121  lspextmo  21125  lsmcl  21152  pj1lmhm  21169  islbs2  21226  issubrgd  21258  dflidl2rng  21290  rnglidlmmgm  21317  rhmpreimaidl  21349  rngqiprnglin  21374  expmhm  21490  nn0srg  21491  prmirredlem  21526  expghm  21529  mulgghm2  21530  domnchr  21586  znf1o  21605  zntoslem  21610  znfld  21614  cygznlem3  21623  phlipf  21706  dsmmlss  21798  uvcf1  21846  frlmlbs  21851  lindff1  21874  lindfrn  21875  f1lindf  21876  issubassa2  21946  mvrf1  22039  mplsubglem  22052  mplsubrg  22058  mplcoe5lem  22094  mplcoe2  22096  mplind  22125  evlslem2  22134  evlseu  22138  mhplss  22222  ply1sclf1  22354  evls1maplmhm  22442  mamucl  22463  mamuass  22464  mamudi  22465  mamudir  22466  mamuvs1  22467  mamuvs2  22468  matbas2d  22485  mamumat1cl  22501  mamulid  22503  mamurid  22504  mat1mhm  22546  dmatid  22557  dmatsubcl  22560  dmatsgrp  22561  dmatmulcl  22562  dmatsrng  22563  dmatcrng  22564  scmatscmiddistr  22570  scmatscm  22575  scmatsgrp  22581  scmatsrng  22582  scmatcrng  22583  scmatsgrp1  22584  scmatsrng1  22585  scmatf1  22593  scmatmhm  22596  mavmul0g  22615  mdet1  22663  mdetunilem9  22682  mdetuni0  22683  mdetmul  22685  madutpos  22704  smadiadetlem4  22731  1elcpmat  22777  cpmatacl  22778  cpmatmcl  22781  mat2pmatf1  22791  mat2pmatmul  22793  mat2pmat1  22794  mat2pmatlin  22797  m2cpm  22803  m2cpminvid  22815  m2cpminvid2  22817  decpmatmul  22834  pmatcollpw1  22838  monmatcollpw  22841  pmatcollpw  22843  pmatcollpw3lem  22845  pmatcollpwscmatlem2  22852  pm2mpf1  22861  mp2pm2mplem4  22871  pm2mpmhmlem2  22881  chp0mat  22908  chpidmat  22909  tgclb  23032  mretopd  23154  toponmre  23155  iscldtop  23157  ordtbaslem  23250  ordtbas2  23253  cnt0  23408  haust1  23414  cnhaus  23416  isreg2  23439  dishaus  23444  ordthaus  23446  dfconn2  23481  iunconn  23490  clsconn  23492  2ndcomap  23520  dis2ndc  23522  llynlly  23539  restnlly  23544  restlly  23545  islly2  23546  llyidm  23550  nllyidm  23551  hausllycmp  23556  kgentopon  23600  txbas  23629  ptbasin2  23640  ptbasfi  23643  txcnp  23682  txcnmpt  23686  pthaus  23700  tx1stc  23712  xkococnlem  23721  xkococn  23722  cnmpt21  23733  qtoptop2  23761  qtopeu  23778  kqt0lem  23798  isr0  23799  regr1lem2  23802  kqreglem1  23803  kqreglem2  23804  kqnrmlem1  23805  kqnrmlem2  23806  nrmr0reg  23811  reghmph  23855  nrmhmph  23856  txswaphmeo  23867  qtophmeo  23879  fbun  23902  trfbas2  23905  isfil2  23918  infil  23925  trfil2  23949  filssufilg  23973  hausflim  24043  fclsnei  24081  fclsfnflim  24089  flimfnfcls  24090  ptcmplem1  24114  clssubg  24171  tgpconncomp  24175  qustgplem  24183  tsmsfbas  24190  utoptop  24296  iducn  24344  cstucnd  24345  isxmetd  24388  isxmet2d  24389  xmettpos  24411  prdsdsf  24429  prdsmet  24432  ressprdsds  24433  imasdsf1olem  24435  imasf1oxmet  24437  imasf1omet  24438  blfvalps  24445  xmetresbl  24499  metss2  24574  comet  24575  stdbdmet  24578  stdbdmopn  24580  methaus  24582  met2ndci  24584  metustfbas  24619  nrmmetd  24636  subgngp  24697  ngptgp  24698  sranlm  24746  nlmvscnlem1  24748  nlmvscn  24749  nrginvrcn  24754  lssnlm  24763  nghmcn  24807  qtopbaslem  24820  reconn  24891  xmetdcn2  24900  metdscn  24919  metnrm  24925  elcncf1di  24959  cncfcdm  24962  mulc1cncf  24969  cncfco  24971  reparphti  25061  isncvsngpd  25214  tcphcph  25301  ipcnlem1  25309  ipcn  25310  iscfil3  25337  bcthlem5  25392  rrxmet  25472  minveclem3  25493  minveclem7  25499  ovolicc2lem4  25584  dyadmbl  25664  volcn  25670  itg1addlem1  25756  itg1addlem2  25761  itg1addlem4  25763  mbfi1fseqlem1  25779  mbfi1fseqlem3  25781  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  dvmptfsum  26039  c1liplem1  26060  dvgt0lem2  26067  ftc1a  26101  ply1domn  26186  ply1divmo  26198  fta1b  26234  ig1peu  26237  coeeu  26287  plydivalg  26365  aaliou2b  26407  ulmss  26462  ulmcn  26464  efif1olem4  26612  efsubm  26618  logccv  26730  logbmpt  26855  logbfval  26857  cvxcl  27051  basellem4  27150  fsumdvdscom  27251  musum  27257  mpodvdsmulf1o  27260  fsumdvdsmul  27261  dvdsmulf1o  27262  dchrelbasd  27305  dchrmulcl  27315  dchrinv  27327  lgsqrlem2  27413  lgsdchr  27421  lgseisenlem2  27442  lgsquadlem1  27446  lgsquadlem2  27447  2sqreulem4  27520  dchrisumlema  27554  dchrisumlem2  27556  chpdifbndlem2  27620  pntpbnd  27654  pntibndlem3  27658  sltsd  27863  oldbday  27996  addsprop  28071  mulcutlem  28226  divsmo  28279  om2noseqf1o  28396  om2noseqiso  28397  axtgcont  28640  tgjustc1  28646  tgjustc2  28647  iscgrglt  28685  ercgrg  28688  idmot  28708  motco  28711  cnvmot  28712  motcgrg  28715  tgisline  28798  tghilberti2  28809  mirreu3  28829  mirmot  28850  ragperp  28892  foot  28897  mideu  28913  midf  28951  lmimot  28973  trgcopyeu  28981  f1otrgds  29071  f1otrg  29073  f1otrge  29074  xmstrkgc  29088  brbtwn2  29108  axlowdimlem15  29159  axcontlem2  29168  axcontlem10  29176  eengtrkg  29189  eengtrkge  29190  numedglnl  29347  usgredgreu  29421  uspgredg2vtxeu  29423  uspgredg2v  29427  usgredg2v  29430  wlkswwlksf1o  30081  wwlksnextinj  30101  clwlkclwwlkf1  30214  clwwlkf1  30253  frcond4  30474  frgrncvvdeqlem8  30510  frgrncvvdeq  30513  frgrwopreglem4  30519  numclwwlk1lem2f1  30561  nrt2irr  30677  grpoinvf  30737  nvmf  30850  vacn  30899  nmcvcn  30900  smcnlem  30902  sspg  30933  ssps  30935  sspmlem  30937  0lno  30995  blocni  31010  ipblnfi  31060  minvecolem7  31088  unopf1o  32121  cnvunop  32123  unoplin  32125  counop  32126  hmopadj2  32146  hmoplin  32147  bralnfn  32153  lnopeq0i  32212  hmops  32225  hmopm  32226  hmopco  32228  lnconi  32238  cnlnadjlem2  32273  adjmul  32297  adjadd  32298  cdjreui  32637  disjxpin  32790  off2  32845  2ndresdju  32853  fnpreimac  32874  suppovss  32885  f1od2  32923  xrofsup  32971  s3f1  33127  ccatf1  33129  swrdf1  33136  odutos  33148  dfmgc2lem  33175  dfmgc2  33176  pwrssmgc  33180  mgcf1o  33183  mndlactf1  33206  mndractf1  33208  abliso  33216  symgcntz  33267  tocyccntz  33326  conjga  33352  fxpsubrg  33356  archiabllem1  33375  archiabllem2  33379  urpropd  33413  elrgspnlem2  33426  rlocf1  33457  rrgsubm  33470  subrdom  33471  ricdomn1  33475  xrge0slmod  33536  nsgmgc  33600  intlidl  33608  idlinsubrg  33619  rhmimaidl  33620  prmidl2  33629  idlmulssprm  33630  isprmidlc  33635  rhmpreimaprmidl  33640  qsidomlem1  33641  qsidomlem2  33642  ssdifidllem  33645  ssdifidlprm  33647  prmidlsubm  33648  mxidlprm  33660  mxidlirredi  33661  ssmxidllem  33663  drnglring  33690  dflringlem2  33693  rsprprmprmidl  33720  rsprprmprmidlb  33721  rprmirred  33729  rprmirredb  33730  1arithufdlem4  33745  selvply1rhmlema  33817  selvply1rhmlem1  33819  mplidomlem  33826  extvfvcl  33835  mplvrpmga  33844  ply1degltdimlem  33921  ply1degltdim  33922  lindsun  33924  fedgmullem1  33928  fedgmullem2  33929  fedgmul  33930  lactlmhm  33933  assalactf1o  33934  minplyirred  34010  constrsdrg  34074  1smat1  34103  submateq  34108  madjusmdetlem3  34128  zart0  34178  pstmxmet  34196  ofcf  34402  ldgenpisys  34465  rossros  34479  inelcarsg  34610  sibfof  34639  sitmf  34651  hgt750lemb  34952  erdszelem4  35549  erdszelem9  35554  erdsze2lem2  35559  cnpconn  35585  pconnconn  35586  txpconn  35587  ptpconn  35588  cvxpconn  35597  cvxsconn  35598  iccllysconn  35605  cvmseu  35631  cvmliftmo  35639  cvmlift2lem5  35662  cvmlift2lem9  35666  mrsubff1  35869  elmrsubrn  35875  mrsubco  35876  msubff1  35911  mvhf1  35914  r1peuqusdeg1  35998  segconeu  36366  nmulprop  36545  fnessref  36722  neibastop1  36724  filnetlem3  36745  onsuct0  36806  weiunlem  36828  mh-inf3f1  36906  unblimceq0lem  36949  unbdqndv2  36954  knoppndv  36977  irrdiff  37823  uncf  38103  fin2so  38111  lindsadd  38117  poimirlem4  38128  poimirlem13  38137  poimirlem14  38138  poimirlem26  38150  heicant  38159  mblfinlem2  38162  ftc1anc  38205  sdclem1  38247  isbnd3  38288  prdsbnd  38297  ismtycnv  38306  ismtyhmeolem  38308  ismtyres  38312  bfplem1  38326  bfplem2  38327  bfp  38328  rrnmet  38333  ismrer1  38342  iccbnd  38344  grpokerinj  38397  isdrngo2  38462  rngogrphom  38475  rngohomco  38478  rngoisocnv  38485  iscringd  38502  eqvreldisj1  39431  erprt  39502  lfl0f  39698  lkrlss  39724  lshpsmreu  39738  linepsubN  40381  pmapsub  40397  lautcnv  40719  lautco  40726  idltrn  40779  cdleme50f1  41172  cdleme50laut  41176  istendod  41391  dihf11  41896  dih1dimatlem  41958  lcfl7N  42130  lcfrlem9  42179  mapd1o  42277  hdmapf1oN  42494  hgmapf1oN  42532  fmpocos  42857  qsalrel  42862  rediveud  43057  imacrhmcl  43141  evlselv  43176  fsuppind  43177  nacsfix  43298  rmxypairf1o  43493  wepwsolem  43624  dnnumch3  43629  fnwe2  43635  mpaaeu  43732  idomsubgmo  43775  mon1psubm  43781  deg1mhm  43782  isotone1  44629  isotone2  44630  mnringmulrcld  44809  traxext  45558  disjxp1  45654  disjf1  45766  wessf1ornlem  45768  projf1o  45779  sumnnodd  46211  lptioo2  46212  lptioo1  46213  cncfshift  46453  cncfperiod  46458  dvnprodlem1  46525  fourierdlem42  46728  nnfoctbdjlem  47034  isomennd  47110  smflimlem6  47355  fsetsnf1  47651  cfsetsnfsetf1  47658  otiunsndisjX  47878  imasetpreimafvbijlemf1  48015  iccpartgt  48038  icceuelpart  48047  ichnreuop  48083  sprsymrelfolem2  48104  sprsymrelf  48106  prproropf1o  48118  reupr  48133  reuopreuprim  48137  uhgrimprop  48519  isuspgrim0lem  48520  upgrimtrls  48533  gpgprismgr4cycllem11  48732  opmpoismgm  48794  mgmplusgiopALT  48821  2zlidl  48867  rhmsubcALTV  48912  srhmsubcALTV  48952  fldhmsubcALTV  48960  lindslinindsimp1  49084  1arymaptf1  49269  2arymaptf1  49280  eqfnovd  49492  fmpodg  49495  toslat  49608  catprsc  49639  catprsc2  49640  oppcendc  49644  invfn  49656  iinfssclem2  49681  iinfssc  49683  iinfsubc  49684  discsubc  49690  nelsubclem  49693  resccatlem  49699  funchomf  49723  imasubclem2  49731  imaidfu  49736  imasubc  49777  imassc  49779  imasubc3  49782  fthcomf  49783  idfth  49784  cofidfth  49788  upeu2  49798  isnatd  49849  swapfffth  49909  diag1f1  49933  diag2f1  49935  fucoppc  50036  isthincd  50062  isthincd2  50063  oppcthinco  50065  oppcthinendcALT  50067  functhinclem4  50073  functhincfun  50075  thincfth  50078  thincciso  50079  thinccisod  50080  functermc  50134  arweuthinc  50155  arweutermc  50156  diagffth  50164  funcsn  50167  0fucterm  50169