Theorem ralrimivva 3178

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

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

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 3045

This theorem is referenced by:  disjord  5091  disjxiun  5099  otsndisj  5474  otiunsndisj  5475  swopo  5550  issod  5574  reuop  6254  fcof1  7244  fliftfund  7270  isof1oidb  7281  isof1oopb  7282  soisores  7284  soisoi  7285  isocnv  7287  f1oiso  7308  oveqrspc2v  7396  oprres  7537  caovclg  7561  caovcomg  7564  off  7651  coof  7657  caofidlcan  7671  caofrss  7672  caonncan  7677  dmmpog  8032  fnmpoovd  8043  fmpoco  8051  fsplitfpar  8074  poxp  8084  fvmpocurryd  8227  smo11  8310  smoiso2  8315  omsmo  8599  nnasmo  8604  coflton  8612  qsdisj2  8745  eroprf  8765  dom2lem  8940  omxpenlem  9019  xpf1o  9080  unxpdomlem3  9175  fofinf1o  9259  dffi3  9358  supmo  9379  infmo  9424  inf3lem6  9564  cantnf  9624  rankxplim  9810  fseqenlem1  9955  fodomacn  9987  iunfictbso  10045  cofsmo  10200  infpssrlem5  10238  enfin2i  10252  fin23lem23  10257  fin23lem27  10259  fin23lem28  10271  compssiso  10305  ltordlem  11681  cju  12160  axdc4uzlem  13926  seqcaopr2  13981  seqhomo  13992  wrd2ind  14665  cshf1  14752  s3sndisj  14910  s3iunsndisj  14911  climcn2  15536  addcn2  15537  mulcn2  15539  o1of2  15556  isercolllem1  15608  fsum2dlem  15713  fsumcom2  15717  fprodser  15892  fprod2dlem  15923  fprodcom2  15927  isprm6  16661  crth  16725  eulerthlem2  16729  vdwlem12  16940  cshwsdisj  17046  imasaddfnlem  17468  imasvscafn  17477  mreexexd  17590  iscatd  17615  oppccomfpropd  17669  isofn  17718  sectmon  17725  ssctr  17768  ssceq  17769  catsubcat  17782  issubc3  17792  fullsubc  17793  fullresc  17794  isfuncd  17808  idfucl  17824  cofucl  17831  funcres2b  17840  fulloppc  17867  fthoppc  17868  idffth  17878  cofull  17879  cofth  17880  ressffth  17883  setcmon  18030  setcepi  18031  resssetc  18035  resscatc  18052  catciso  18054  fthestrcsetc  18092  fullestrcsetc  18093  embedsetcestrclem  18099  fthsetcestrc  18107  fullsetcestrc  18108  evlfcl  18164  uncfcurf  18181  hofcl  18201  yonedalem3  18222  yonedainv  18223  yonffthlem  18224  yoniso  18227  isdrs2  18248  isposd  18264  pospropd  18267  poslubmo  18351  posglbmo  18352  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  19075  nsgacs  19077  0nsg  19084  nsgid  19085  qus0subgadd  19114  cycsubmcom  19119  isghmd  19140  ghmmhm  19141  idghm  19146  ghmnsgima  19155  ghmnsgpreima  19156  ghmf1  19161  kerf1ghm  19162  ghmf1o  19163  gaid  19214  subgga  19215  gass  19216  gasubg  19217  cntzsgrpcl  19249  cntzsubm  19253  cntrsubgnsg  19258  lactghmga  19320  symgfixf1  19352  odf1  19477  sylow1lem2  19514  sylow2blem2  19536  sylow3lem1  19542  lsmssv  19558  smndlsmidm  19571  pj1eu  19611  efglem  19631  efgtf  19637  efgred  19663  efgredeu  19667  frgpmhm  19680  frgpuptf  19685  frgpuplem  19687  mulgmhm  19742  ghmcmn  19746  invghm  19748  ablnsg  19762  imasabl  19791  cygabl  19806  gsum2d2lem  19888  gsum2d2  19889  gsumcom2  19890  dprd2d2  19961  ablfaclem2  20003  srgfcl  20117  srgcom4lem  20134  srglmhm  20142  srgrmhm  20143  ringcomlem  20200  isrnghm2d  20371  c0mgm  20380  c0mhm  20381  isrhm2d  20408  subrngringnsg  20474  issubrng2  20479  subrngint  20481  issubrg2  20513  subrgint  20516  rnghmsscmap2  20550  rnghmsscmap  20551  rnghmsubcsetclem2  20553  rhmsscmap2  20579  rhmsscmap  20580  rhmsubcsetclem2  20582  rhmsscrnghm  20586  rhmsubcrngclem2  20588  srhmsubc  20601  rhmsubc  20610  fldhmsubc  20706  primefld  20726  abvn0b  20757  suborng  20797  islmodd  20805  lmodscaf  20823  lmodprop2d  20863  islssd  20874  islss4  20901  lssacs  20906  lsspropd  20957  islmhmd  20979  lmhmima  20987  lmhmpreima  20988  reslmhm  20992  lspextmo  20996  lsmcl  21023  pj1lmhm  21040  islbs2  21097  issubrgd  21129  dflidl2rng  21161  rnglidlmmgm  21188  rhmpreimaidl  21220  rngqiprnglin  21245  expmhm  21379  nn0srg  21380  prmirredlem  21415  expghm  21418  mulgghm2  21419  domnchr  21475  znf1o  21494  zntoslem  21499  znfld  21503  cygznlem3  21512  phlipf  21595  dsmmlss  21687  uvcf1  21735  frlmlbs  21740  lindff1  21763  lindfrn  21764  f1lindf  21765  issubassa2  21835  mvrf1  21929  mplsubglem  21942  mplsubrg  21948  mplcoe5lem  21980  mplcoe2  21982  mplind  22011  evlslem2  22020  evlseu  22024  mhplss  22076  ply1sclf1  22209  evls1maplmhm  22298  mamucl  22322  mamuass  22323  mamudi  22324  mamudir  22325  mamuvs1  22326  mamuvs2  22327  matbas2d  22344  mamumat1cl  22360  mamulid  22362  mamurid  22363  mat1mhm  22405  dmatid  22416  dmatsubcl  22419  dmatsgrp  22420  dmatmulcl  22421  dmatsrng  22422  dmatcrng  22423  scmatscmiddistr  22429  scmatscm  22434  scmatsgrp  22440  scmatsrng  22441  scmatcrng  22442  scmatsgrp1  22443  scmatsrng1  22444  scmatf1  22452  scmatmhm  22455  mavmul0g  22474  mdet1  22522  mdetunilem9  22541  mdetuni0  22542  mdetmul  22544  madutpos  22563  smadiadetlem4  22590  1elcpmat  22636  cpmatacl  22637  cpmatmcl  22640  mat2pmatf1  22650  mat2pmatmul  22652  mat2pmat1  22653  mat2pmatlin  22656  m2cpm  22662  m2cpminvid  22674  m2cpminvid2  22676  decpmatmul  22693  pmatcollpw1  22697  monmatcollpw  22700  pmatcollpw  22702  pmatcollpw3lem  22704  pmatcollpwscmatlem2  22711  pm2mpf1  22720  mp2pm2mplem4  22730  pm2mpmhmlem2  22740  chp0mat  22767  chpidmat  22768  tgclb  22891  mretopd  23013  toponmre  23014  iscldtop  23016  ordtbaslem  23109  ordtbas2  23112  cnt0  23267  haust1  23273  cnhaus  23275  isreg2  23298  dishaus  23303  ordthaus  23305  dfconn2  23340  iunconn  23349  clsconn  23351  2ndcomap  23379  dis2ndc  23381  llynlly  23398  restnlly  23403  restlly  23404  islly2  23405  llyidm  23409  nllyidm  23410  hausllycmp  23415  kgentopon  23459  txbas  23488  ptbasin2  23499  ptbasfi  23502  txcnp  23541  txcnmpt  23545  pthaus  23559  tx1stc  23571  xkococnlem  23580  xkococn  23581  cnmpt21  23592  qtoptop2  23620  qtopeu  23637  kqt0lem  23657  isr0  23658  regr1lem2  23661  kqreglem1  23662  kqreglem2  23663  kqnrmlem1  23664  kqnrmlem2  23665  nrmr0reg  23670  reghmph  23714  nrmhmph  23715  txswaphmeo  23726  qtophmeo  23738  fbun  23761  trfbas2  23764  isfil2  23777  infil  23784  trfil2  23808  filssufilg  23832  hausflim  23902  fclsnei  23940  fclsfnflim  23948  flimfnfcls  23949  ptcmplem1  23973  clssubg  24030  tgpconncomp  24034  qustgplem  24042  tsmsfbas  24049  utoptop  24156  iducn  24204  cstucnd  24205  isxmetd  24248  isxmet2d  24249  xmettpos  24271  prdsdsf  24289  prdsmet  24292  ressprdsds  24293  imasdsf1olem  24295  imasf1oxmet  24297  imasf1omet  24298  blfvalps  24305  xmetresbl  24359  metss2  24434  comet  24435  stdbdmet  24438  stdbdmopn  24440  methaus  24442  met2ndci  24444  metustfbas  24479  nrmmetd  24496  subgngp  24557  ngptgp  24558  sranlm  24606  nlmvscnlem1  24608  nlmvscn  24609  nrginvrcn  24614  lssnlm  24623  nghmcn  24667  qtopbaslem  24680  reconn  24751  xmetdcn2  24760  metdscn  24779  metnrm  24785  elcncf1di  24822  cncfcdm  24825  mulc1cncf  24832  cncfco  24834  reparphti  24930  reparphtiOLD  24931  isncvsngpd  25084  tcphcph  25171  ipcnlem1  25179  ipcn  25180  iscfil3  25207  bcthlem5  25262  rrxmet  25342  minveclem3  25363  minveclem7  25369  ovolicc2lem4  25455  dyadmbl  25535  volcn  25541  itg1addlem1  25627  itg1addlem2  25632  itg1addlem4  25634  mbfi1fseqlem1  25650  mbfi1fseqlem3  25652  mbfi1fseqlem4  25653  mbfi1fseqlem5  25654  dvmptfsum  25913  c1liplem1  25935  dvgt0lem2  25942  ftc1a  25978  ply1domn  26063  ply1divmo  26075  fta1b  26111  ig1peu  26114  coeeu  26164  plydivalg  26241  aaliou2b  26283  ulmss  26340  ulmcn  26342  efif1olem4  26488  efsubm  26494  logccv  26606  logbmpt  26732  logbfval  26734  cvxcl  26929  basellem4  27028  fsumdvdscom  27129  musum  27135  mpodvdsmulf1o  27138  fsumdvdsmul  27139  dvdsmulf1o  27140  fsumdvdsmulOLD  27141  dchrelbasd  27184  dchrmulcl  27194  dchrinv  27206  lgsqrlem2  27292  lgsdchr  27300  lgseisenlem2  27321  lgsquadlem1  27325  lgsquadlem2  27326  2sqreulem4  27399  dchrisumlema  27433  dchrisumlem2  27435  chpdifbndlem2  27499  pntpbnd  27533  pntibndlem3  27537  ssltd  27738  oldbday  27851  addsprop  27924  mulscutlem  28075  divsmo  28128  om2noseqf1o  28236  om2noseqiso  28237  axtgcont  28450  tgjustc1  28456  tgjustc2  28457  iscgrglt  28495  ercgrg  28498  idmot  28518  motco  28521  cnvmot  28522  motcgrg  28525  tgisline  28608  tghilberti2  28619  mirreu3  28635  mirmot  28656  ragperp  28698  foot  28703  mideu  28719  midf  28757  lmimot  28779  trgcopyeu  28787  f1otrgds  28850  f1otrg  28852  f1otrge  28853  xmstrkgc  28867  brbtwn2  28886  axlowdimlem15  28937  axcontlem2  28946  axcontlem10  28954  eengtrkg  28967  eengtrkge  28968  numedglnl  29125  usgredgreu  29199  uspgredg2vtxeu  29201  uspgredg2v  29205  usgredg2v  29208  wlkswwlksf1o  29860  wwlksnextinj  29880  clwlkclwwlkf1  29990  clwwlkf1  30029  frcond4  30250  frgrncvvdeqlem8  30286  frgrncvvdeq  30289  frgrwopreglem4  30295  numclwwlk1lem2f1  30337  nrt2irr  30453  grpoinvf  30512  nvmf  30625  vacn  30674  nmcvcn  30675  smcnlem  30677  sspg  30708  ssps  30710  sspmlem  30712  0lno  30770  blocni  30785  ipblnfi  30835  minvecolem7  30863  unopf1o  31896  cnvunop  31898  unoplin  31900  counop  31901  hmopadj2  31921  hmoplin  31922  bralnfn  31928  lnopeq0i  31987  hmops  32000  hmopm  32001  hmopco  32003  lnconi  32013  cnlnadjlem2  32048  adjmul  32072  adjadd  32073  cdjreui  32412  disjxpin  32568  off2  32616  2ndresdju  32624  fnpreimac  32646  suppovss  32655  f1od2  32695  xrofsup  32741  s3f1  32919  ccatf1  32921  swrdf1  32929  odutos  32941  dfmgc2lem  32968  dfmgc2  32969  pwrssmgc  32973  mgcf1o  32976  mndlactf1  33011  mndractf1  33013  abliso  33021  symgcntz  33058  tocyccntz  33117  conjga  33143  archiabllem1  33163  archiabllem2  33167  urpropd  33200  elrgspnlem2  33211  rlocf1  33241  rrgsubm  33251  subrdom  33252  xrge0slmod  33313  nsgmgc  33377  intlidl  33385  idlinsubrg  33396  rhmimaidl  33397  prmidl2  33406  idlmulssprm  33407  isprmidlc  33412  rhmpreimaprmidl  33416  qsidomlem1  33417  qsidomlem2  33418  ssdifidllem  33421  ssdifidlprm  33423  mxidlprm  33435  mxidlirredi  33436  ssmxidllem  33438  rsprprmprmidl  33487  rsprprmprmidlb  33488  rprmirred  33496  rprmirredb  33497  1arithufdlem4  33512  ply1degltdimlem  33612  ply1degltdim  33613  lindsun  33615  fedgmullem1  33619  fedgmullem2  33620  fedgmul  33621  lactlmhm  33624  assalactf1o  33625  minplyirred  33695  constrsdrg  33759  1smat1  33788  submateq  33793  madjusmdetlem3  33813  zart0  33863  pstmxmet  33881  ofcf  34087  ldgenpisys  34150  rossros  34164  inelcarsg  34296  sibfof  34325  sitmf  34337  hgt750lemb  34641  erdszelem4  35175  erdszelem9  35180  erdsze2lem2  35185  cnpconn  35211  pconnconn  35212  txpconn  35213  ptpconn  35214  cvxpconn  35223  cvxsconn  35224  iccllysconn  35231  cvmseu  35257  cvmliftmo  35265  cvmlift2lem5  35288  cvmlift2lem9  35292  mrsubff1  35495  elmrsubrn  35501  mrsubco  35502  msubff1  35537  mvhf1  35540  r1peuqusdeg1  35624  segconeu  35993  fnessref  36339  neibastop1  36341  filnetlem3  36362  onsuct0  36423  weiunlem2  36445  unblimceq0lem  36488  unbdqndv2  36493  knoppndv  36516  irrdiff  37308  uncf  37587  fin2so  37595  lindsadd  37601  poimirlem4  37612  poimirlem13  37621  poimirlem14  37622  poimirlem26  37634  heicant  37643  mblfinlem2  37646  ftc1anc  37689  sdclem1  37731  isbnd3  37772  prdsbnd  37781  ismtycnv  37790  ismtyhmeolem  37792  ismtyres  37796  bfplem1  37810  bfplem2  37811  bfp  37812  rrnmet  37817  ismrer1  37826  iccbnd  37828  grpokerinj  37881  isdrngo2  37946  rngogrphom  37959  rngohomco  37962  rngoisocnv  37969  iscringd  37986  eqvreldisj1  38810  erprt  38860  lfl0f  39056  lkrlss  39082  lshpsmreu  39096  linepsubN  39740  pmapsub  39756  lautcnv  40078  lautco  40085  idltrn  40138  cdleme50f1  40531  cdleme50laut  40535  istendod  40750  dihf11  41255  dih1dimatlem  41317  lcfl7N  41489  lcfrlem9  41538  mapd1o  41636  hdmapf1oN  41853  hgmapf1oN  41891  fmpocos  42216  qsalrel  42222  rediveud  42425  imacrhmcl  42496  evlselv  42569  fsuppind  42572  nacsfix  42694  rmxypairf1o  42894  wepwsolem  43025  dnnumch3  43030  fnwe2  43036  mpaaeu  43133  idomsubgmo  43176  mon1psubm  43182  deg1mhm  43183  isotone1  44031  isotone2  44032  mnringmulrcld  44211  traxext  44961  disjxp1  45057  disjf1  45171  wessf1ornlem  45173  projf1o  45185  sumnnodd  45622  lptioo2  45623  lptioo1  45624  cncfshift  45866  cncfperiod  45871  dvnprodlem1  45938  fourierdlem42  46141  nnfoctbdjlem  46447  isomennd  46523  smflimlem6  46768  fsetsnf1  47047  cfsetsnfsetf1  47054  otiunsndisjX  47274  imasetpreimafvbijlemf1  47399  iccpartgt  47422  icceuelpart  47431  ichnreuop  47467  sprsymrelfolem2  47488  sprsymrelf  47490  prproropf1o  47502  reupr  47517  reuopreuprim  47521  uhgrimprop  47886  isuspgrim0lem  47887  upgrimtrls  47900  gpgprismgr4cycllem11  48089  opmpoismgm  48149  mgmplusgiopALT  48176  2zlidl  48222  rhmsubcALTV  48267  srhmsubcALTV  48307  fldhmsubcALTV  48315  lindslinindsimp1  48440  1arymaptf1  48625  2arymaptf1  48636  eqfnovd  48848  fmpodg  48851  toslat  48964  catprsc  48996  catprsc2  48997  oppcendc  49001  invfn  49013  iinfssclem2  49038  iinfssc  49040  iinfsubc  49041  discsubc  49047  nelsubclem  49050  resccatlem  49056  funchomf  49080  imasubclem2  49088  imaidfu  49093  imasubc  49134  imassc  49136  imasubc3  49139  fthcomf  49140  idfth  49141  cofidfth  49145  upeu2  49155  isnatd  49206  swapfffth  49266  diag1f1  49290  diag2f1  49292  fucoppc  49393  isthincd  49419  isthincd2  49420  oppcthinco  49422  oppcthinendcALT  49424  functhinclem4  49430  functhincfun  49432  thincfth  49435  thincciso  49436  thinccisod  49437  functermc  49491  arweuthinc  49512  arweutermc  49513  diagffth  49521  funcsn  49524  0fucterm  49526