Theorem ralrimivva 3199

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  disjord  5136  disjxiun  5144  otsndisj  5528  otiunsndisj  5529  swopo  5607  issod  5630  reuop  6314  fcof1  7306  fliftfund  7332  isof1oidb  7343  isof1oopb  7344  soisores  7346  soisoi  7347  isocnv  7349  f1oiso  7370  oveqrspc2v  7457  oprres  7600  caovclg  7624  caovcomg  7627  off  7714  coof  7720  caofrss  7734  caonncan  7739  dmmpog  8097  fnmpoovd  8110  fmpoco  8118  fsplitfpar  8141  poxp  8151  fvmpocurryd  8294  smo11  8402  smoiso2  8407  omsmo  8694  nnasmo  8699  coflton  8707  qsdisj2  8833  eroprf  8853  dom2lem  9030  omxpenlem  9111  xpf1o  9177  unxpdomlem3  9285  fofinf1o  9369  dffi3  9468  supmo  9489  infmo  9532  inf3lem6  9670  cantnf  9730  rankxplim  9916  fseqenlem1  10061  fodomacn  10093  iunfictbso  10151  cofsmo  10306  infpssrlem5  10344  enfin2i  10358  fin23lem23  10363  fin23lem27  10365  fin23lem28  10377  compssiso  10411  ltordlem  11785  cju  12259  axdc4uzlem  14020  seqcaopr2  14075  seqhomo  14086  wrd2ind  14757  cshf1  14844  s3sndisj  15002  s3iunsndisj  15003  climcn2  15625  addcn2  15626  mulcn2  15628  o1of2  15645  isercolllem1  15697  fsum2dlem  15802  fsumcom2  15806  fprodser  15981  fprod2dlem  16012  fprodcom2  16016  isprm6  16747  crth  16811  eulerthlem2  16815  vdwlem12  17025  cshwsdisj  17132  imasaddfnlem  17574  imasvscafn  17583  mreexexd  17692  iscatd  17717  oppccomfpropd  17773  isofn  17822  sectmon  17829  ssctr  17872  ssceq  17873  catsubcat  17889  issubc3  17899  fullsubc  17900  fullresc  17901  isfuncd  17915  idfucl  17931  cofucl  17938  funcres2b  17947  fulloppc  17975  fthoppc  17976  idffth  17986  cofull  17987  cofth  17988  ressffth  17991  setcmon  18140  setcepi  18141  resssetc  18145  resscatc  18162  catciso  18164  fthestrcsetc  18205  fullestrcsetc  18206  embedsetcestrclem  18212  fthsetcestrc  18220  fullsetcestrc  18221  evlfcl  18278  uncfcurf  18295  hofcl  18315  yonedalem3  18336  yonedainv  18337  yonffthlem  18338  yoniso  18341  isdrs2  18363  isposd  18380  pospropd  18384  poslubmo  18468  posglbmo  18469  mgmplusf  18675  ismgmd  18677  issstrmgm  18678  opifismgm  18684  mgmhmpropd  18723  mgmhmf1o  18725  idmgmhm  18726  issubmgm2  18728  rabsubmgmd  18729  resmgmhm  18736  resmgmhm2  18737  resmgmhm2b  18738  mgmhmco  18739  submgmacs  18742  issgrpd  18755  sgrppropd  18756  ismndd  18781  mndpropd  18784  issubmnd  18786  mndinvmod  18789  ismhmd  18811  mhmpropd  18817  idmhm  18820  mhmf1o  18821  issubmd  18831  mndissubm  18832  0mhm  18844  resmhm  18845  resmhm2  18846  resmhm2b  18847  mhmco  18848  submacs  18852  prdspjmhm  18854  pwsdiagmhm  18856  pwsco1mhm  18857  pwsco2mhm  18858  gsumwspan  18871  frmdsssubm  18886  frmdup1  18889  grpsubf  19049  dfgrp3  19069  mhmmnd  19094  mhmfmhm  19095  issubg4  19175  grpissubg  19176  isnsg3  19190  nsgacs  19192  0nsg  19199  nsgid  19200  qus0subgadd  19229  cycsubmcom  19234  isghmd  19255  ghmmhm  19256  idghm  19261  ghmnsgima  19270  ghmnsgpreima  19271  ghmf1  19276  kerf1ghm  19277  ghmf1o  19278  gaid  19329  subgga  19330  gass  19331  gasubg  19332  cntzsgrpcl  19364  cntzsubm  19368  cntrsubgnsg  19373  lactghmga  19437  symgfixf1  19469  odf1  19594  sylow1lem2  19631  sylow2blem2  19653  sylow3lem1  19659  lsmssv  19675  smndlsmidm  19688  pj1eu  19728  efglem  19748  efgtf  19754  efgred  19780  efgredeu  19784  frgpmhm  19797  frgpuptf  19802  frgpuplem  19804  mulgmhm  19859  ghmcmn  19863  invghm  19865  ablnsg  19879  imasabl  19908  cygabl  19923  gsum2d2lem  20005  gsum2d2  20006  gsumcom2  20007  dprd2d2  20078  ablfaclem2  20120  srgfcl  20213  srgcom4lem  20230  srglmhm  20238  srgrmhm  20239  ringcomlem  20292  isrnghm2d  20466  c0mgm  20475  c0mhm  20476  isrhm2d  20503  subrngringnsg  20569  issubrng2  20574  subrngint  20576  issubrg2  20608  subrgint  20611  rnghmsscmap2  20645  rnghmsscmap  20646  rnghmsubcsetclem2  20648  rhmsscmap2  20674  rhmsscmap  20675  rhmsubcsetclem2  20677  rhmsscrnghm  20681  rhmsubcrngclem2  20683  srhmsubc  20696  rhmsubc  20705  fldhmsubc  20802  primefld  20822  abvn0b  20853  islmodd  20880  lmodscaf  20898  lmodprop2d  20938  islssd  20950  islss4  20977  lssacs  20982  lsspropd  21033  islmhmd  21055  lmhmima  21063  lmhmpreima  21064  reslmhm  21068  lspextmo  21072  lsmcl  21099  pj1lmhm  21116  islbs2  21173  issubrgd  21213  dflidl2rng  21245  rnglidlmmgm  21272  rhmpreimaidl  21304  rngqiprnglin  21329  expmhm  21471  nn0srg  21472  prmirredlem  21500  expghm  21503  mulgghm2  21504  domnchr  21564  znf1o  21587  zntoslem  21592  znfld  21596  cygznlem3  21605  phlipf  21687  dsmmlss  21781  uvcf1  21829  frlmlbs  21834  lindff1  21857  lindfrn  21858  f1lindf  21859  issubassa2  21929  mvrf1  22023  mplsubglem  22036  mplsubrg  22042  mplcoe5lem  22074  mplcoe2  22076  mplind  22111  evlslem2  22120  evlseu  22124  mhplss  22176  ply1sclf1  22307  evls1maplmhm  22396  mamucl  22420  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  matbas2d  22444  mamumat1cl  22460  mamulid  22462  mamurid  22463  mat1mhm  22505  dmatid  22516  dmatsubcl  22519  dmatsgrp  22520  dmatmulcl  22521  dmatsrng  22522  dmatcrng  22523  scmatscmiddistr  22529  scmatscm  22534  scmatsgrp  22540  scmatsrng  22541  scmatcrng  22542  scmatsgrp1  22543  scmatsrng1  22544  scmatf1  22552  scmatmhm  22555  mavmul0g  22574  mdet1  22622  mdetunilem9  22641  mdetuni0  22642  mdetmul  22644  madutpos  22663  smadiadetlem4  22690  1elcpmat  22736  cpmatacl  22737  cpmatmcl  22740  mat2pmatf1  22750  mat2pmatmul  22752  mat2pmat1  22753  mat2pmatlin  22756  m2cpm  22762  m2cpminvid  22774  m2cpminvid2  22776  decpmatmul  22793  pmatcollpw1  22797  monmatcollpw  22800  pmatcollpw  22802  pmatcollpw3lem  22804  pmatcollpwscmatlem2  22811  pm2mpf1  22820  mp2pm2mplem4  22830  pm2mpmhmlem2  22840  chp0mat  22867  chpidmat  22868  tgclb  22992  mretopd  23115  toponmre  23116  iscldtop  23118  ordtbaslem  23211  ordtbas2  23214  cnt0  23369  haust1  23375  cnhaus  23377  isreg2  23400  dishaus  23405  ordthaus  23407  dfconn2  23442  iunconn  23451  clsconn  23453  2ndcomap  23481  dis2ndc  23483  llynlly  23500  restnlly  23505  restlly  23506  islly2  23507  llyidm  23511  nllyidm  23512  hausllycmp  23517  kgentopon  23561  txbas  23590  ptbasin2  23601  ptbasfi  23604  txcnp  23643  txcnmpt  23647  pthaus  23661  tx1stc  23673  xkococnlem  23682  xkococn  23683  cnmpt21  23694  qtoptop2  23722  qtopeu  23739  kqt0lem  23759  isr0  23760  regr1lem2  23763  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  nrmr0reg  23772  reghmph  23816  nrmhmph  23817  txswaphmeo  23828  qtophmeo  23840  fbun  23863  trfbas2  23866  isfil2  23879  infil  23886  trfil2  23910  filssufilg  23934  hausflim  24004  fclsnei  24042  fclsfnflim  24050  flimfnfcls  24051  ptcmplem1  24075  clssubg  24132  tgpconncomp  24136  qustgplem  24144  tsmsfbas  24151  utoptop  24258  iducn  24307  cstucnd  24308  isxmetd  24351  isxmet2d  24352  xmettpos  24374  prdsdsf  24392  prdsmet  24395  ressprdsds  24396  imasdsf1olem  24398  imasf1oxmet  24400  imasf1omet  24401  blfvalps  24408  xmetresbl  24462  metss2  24540  comet  24541  stdbdmet  24544  stdbdmopn  24546  methaus  24548  met2ndci  24550  metustfbas  24585  nrmmetd  24602  subgngp  24663  ngptgp  24664  sranlm  24720  nlmvscnlem1  24722  nlmvscn  24723  nrginvrcn  24728  lssnlm  24737  nghmcn  24781  qtopbaslem  24794  reconn  24863  xmetdcn2  24872  metdscn  24891  metnrm  24897  elcncf1di  24934  cncfcdm  24937  mulc1cncf  24944  cncfco  24946  reparphti  25042  reparphtiOLD  25043  isncvsngpd  25197  tcphcph  25284  ipcnlem1  25292  ipcn  25293  iscfil3  25320  bcthlem5  25375  rrxmet  25455  minveclem3  25476  minveclem7  25482  ovolicc2lem4  25568  dyadmbl  25648  volcn  25654  itg1addlem1  25740  itg1addlem2  25745  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  dvmptfsum  26027  c1liplem1  26049  dvgt0lem2  26056  ftc1a  26092  ply1domn  26177  ply1divmo  26189  fta1b  26225  ig1peu  26228  coeeu  26278  plydivalg  26355  aaliou2b  26397  ulmss  26454  ulmcn  26456  efif1olem4  26601  efsubm  26607  logccv  26719  logbmpt  26845  logbfval  26847  cvxcl  27042  basellem4  27141  fsumdvdscom  27242  musum  27248  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  dchrelbasd  27297  dchrmulcl  27307  dchrinv  27319  lgsqrlem2  27405  lgsdchr  27413  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  2sqreulem4  27512  dchrisumlema  27546  dchrisumlem2  27548  chpdifbndlem2  27612  pntpbnd  27646  pntibndlem3  27650  ssltd  27850  oldbday  27953  addsprop  28023  mulscutlem  28171  divsmo  28224  om2noseqf1o  28321  om2noseqiso  28322  axtgcont  28491  tgjustc1  28497  tgjustc2  28498  iscgrglt  28536  ercgrg  28539  idmot  28559  motco  28562  cnvmot  28563  motcgrg  28566  tgisline  28649  tghilberti2  28660  mirreu3  28676  mirmot  28697  ragperp  28739  foot  28744  mideu  28760  midf  28798  lmimot  28820  trgcopyeu  28828  f1otrgds  28891  f1otrg  28893  f1otrge  28894  xmstrkgc  28914  brbtwn2  28934  axlowdimlem15  28985  axcontlem2  28994  axcontlem10  29002  eengtrkg  29015  eengtrkge  29016  numedglnl  29175  usgredgreu  29249  uspgredg2vtxeu  29251  uspgredg2v  29255  usgredg2v  29258  wlkswwlksf1o  29908  wwlksnextinj  29928  clwlkclwwlkf1  30038  clwwlkf1  30077  frcond4  30298  frgrncvvdeqlem8  30334  frgrncvvdeq  30337  frgrwopreglem4  30343  numclwwlk1lem2f1  30385  nrt2irr  30501  grpoinvf  30560  nvmf  30673  vacn  30722  nmcvcn  30723  smcnlem  30725  sspg  30756  ssps  30758  sspmlem  30760  0lno  30818  blocni  30833  ipblnfi  30883  minvecolem7  30911  unopf1o  31944  cnvunop  31946  unoplin  31948  counop  31949  hmopadj2  31969  hmoplin  31970  bralnfn  31976  lnopeq0i  32035  hmops  32048  hmopm  32049  hmopco  32051  lnconi  32061  cnlnadjlem2  32096  adjmul  32120  adjadd  32121  cdjreui  32460  disjxpin  32607  off2  32657  2ndresdju  32665  fnpreimac  32687  suppovss  32695  f1od2  32738  xrofsup  32777  s3f1  32915  ccatf1  32917  swrdf1  32925  odutos  32942  dfmgc2lem  32969  dfmgc2  32970  pwrssmgc  32974  mgcf1o  32977  mndlactf1  33013  mndractf1  33015  abliso  33023  symgcntz  33087  tocyccntz  33146  archiabllem1  33182  archiabllem2  33186  urpropd  33221  elrgspnlem2  33232  rlocf1  33259  rrgsubm  33267  subrdom  33268  suborng  33324  xrge0slmod  33355  nsgmgc  33419  intlidl  33427  idlinsubrg  33438  rhmimaidl  33439  prmidl2  33448  idlmulssprm  33449  isprmidlc  33454  rhmpreimaprmidl  33458  qsidomlem1  33459  qsidomlem2  33460  ssdifidllem  33463  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  ssmxidllem  33480  rsprprmprmidl  33529  rsprprmprmidlb  33530  rprmirred  33538  rprmirredb  33539  1arithufdlem4  33554  ply1degltdimlem  33649  ply1degltdim  33650  lindsun  33652  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  lactlmhm  33661  assalactf1o  33662  minplyirred  33718  1smat1  33764  submateq  33769  madjusmdetlem3  33789  zart0  33839  pstmxmet  33857  ofcf  34083  ldgenpisys  34146  rossros  34160  inelcarsg  34292  sibfof  34321  sitmf  34333  hgt750lemb  34649  erdszelem4  35178  erdszelem9  35183  erdsze2lem2  35188  cnpconn  35214  pconnconn  35215  txpconn  35216  ptpconn  35217  cvxpconn  35226  cvxsconn  35227  iccllysconn  35234  cvmseu  35260  cvmliftmo  35268  cvmlift2lem5  35291  cvmlift2lem9  35295  mrsubff1  35498  elmrsubrn  35504  mrsubco  35505  msubff1  35540  mvhf1  35543  r1peuqusdeg1  35627  segconeu  35992  fnessref  36339  neibastop1  36341  filnetlem3  36362  onsuct0  36423  weiunlem2  36445  unblimceq0lem  36488  unbdqndv2  36493  knoppndv  36516  irrdiff  37308  uncf  37585  fin2so  37593  lindsadd  37599  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  poimirlem26  37632  heicant  37641  mblfinlem2  37644  ftc1anc  37687  sdclem1  37729  isbnd3  37770  prdsbnd  37779  ismtycnv  37788  ismtyhmeolem  37790  ismtyres  37794  bfplem1  37808  bfplem2  37809  bfp  37810  rrnmet  37815  ismrer1  37824  iccbnd  37826  grpokerinj  37879  isdrngo2  37944  rngogrphom  37957  rngohomco  37960  rngoisocnv  37967  iscringd  37984  eqvreldisj1  38805  erprt  38854  lfl0f  39050  lkrlss  39076  lshpsmreu  39090  linepsubN  39734  pmapsub  39750  lautcnv  40072  lautco  40079  idltrn  40132  cdleme50f1  40525  cdleme50laut  40529  istendod  40744  dihf11  41249  dih1dimatlem  41311  lcfl7N  41483  lcfrlem9  41532  mapd1o  41630  hdmapf1oN  41847  hgmapf1oN  41885  fmpocos  42253  qsalrel  42259  imacrhmcl  42500  evlselv  42573  fsuppind  42576  nacsfix  42699  rmxypairf1o  42899  wepwsolem  43030  dnnumch3  43035  fnwe2  43041  mpaaeu  43138  idomsubgmo  43181  mon1psubm  43187  deg1mhm  43188  isotone1  44037  isotone2  44038  mnringmulrcld  44223  traxext  44937  disjxp1  45008  disjf1  45125  wessf1ornlem  45127  projf1o  45139  sumnnodd  45585  lptioo2  45586  lptioo1  45587  cncfshift  45829  cncfperiod  45834  dvnprodlem1  45901  fourierdlem42  46104  nnfoctbdjlem  46410  isomennd  46486  smflimlem6  46731  fsetsnf1  47001  cfsetsnfsetf1  47008  otiunsndisjX  47228  imasetpreimafvbijlemf1  47328  iccpartgt  47351  icceuelpart  47360  ichnreuop  47396  sprsymrelfolem2  47417  sprsymrelf  47419  prproropf1o  47431  reupr  47446  reuopreuprim  47450  isuspgrim0lem  47808  uspgrimprop  47810  opmpoismgm  48010  mgmplusgiopALT  48037  2zlidl  48083  rhmsubcALTV  48128  srhmsubcALTV  48168  fldhmsubcALTV  48176  lindslinindsimp1  48302  1arymaptf1  48491  2arymaptf1  48502  toslat  48770  catprsc  48801  catprsc2  48802  upeu2  48817  isthincd  48836  isthincd2  48837  functhinclem4  48843  thincfth  48847  thincciso  48848  thinccisod  48849