Theorem ralrimivva 2971

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	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )

Assertion

Ref	Expression
ralrimivva	|- ( ph -> A. x e. A A. y e. B ps )

Distinct variable groups:   ph, x, y   y, A

Allowed substitution hints:   ps( x, y)   A( x)   B( x, y)

Proof of Theorem ralrimivva

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )
2	1	ex 450	. 2 |- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )
3	2	ralrimivv 2970	1 |- ( ph -> A. x e. A A. y e. B ps )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  disjord  4641  disjxiun  4649  disjxiunOLD  4650  otsndisj  4979  otiunsndisj  4980  swopo  5045  issod  5065  fcof1  6542  fliftfund  6563  isof1oidb  6574  isof1oopb  6575  soisores  6577  soisoi  6578  isocnv  6580  f1oiso  6601  oveqrspc2v  6673  oprres  6802  caovclg  6826  caovcomg  6829  off  6912  caofrss  6930  caonncan  6935  dmmpt2g  7243  fnmpt2ovd  7252  fmpt2co  7260  poxp  7289  fvmpt2curryd  7397  smo11  7461  smoiso2  7466  omsmo  7734  qsdisj2  7825  eroprf  7845  dom2lem  7995  omxpenlem  8061  xpf1o  8122  unxpdomlem3  8166  fofinf1o  8241  dffi3  8337  supmo  8358  infmo  8401  inf3lem6  8530  cantnf  8590  rankxplim  8742  fseqenlem1  8847  fodomacn  8879  iunfictbso  8937  cofsmo  9091  infpssrlem5  9129  enfin2i  9143  fin23lem23  9148  fin23lem27  9150  fin23lem28  9162  compssiso  9196  ltordlem  10553  cju  11016  axdc4uzlem  12782  seqcaopr2  12837  seqhomo  12848  wrd2ind  13477  cshf1  13556  s3sndisj  13706  s3iunsndisj  13707  climcn2  14323  addcn2  14324  mulcn2  14326  o1of2  14343  isercolllem1  14395  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fprodser  14679  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  isprm6  15426  crth  15483  eulerthlem2  15487  vdwlem12  15696  cshwsdisj  15805  imasaddfnlem  16188  imasvscafn  16197  mreexexd  16308  mreexexdOLD  16309  iscatd  16334  oppccomfpropd  16387  isofn  16435  sectmon  16442  ssctr  16485  ssceq  16486  catsubcat  16499  issubc3  16509  fullsubc  16510  fullresc  16511  isfuncd  16525  idfucl  16541  cofucl  16548  funcres2b  16557  fulloppc  16582  fthoppc  16583  idffth  16593  cofull  16594  cofth  16595  ressffth  16598  setcmon  16737  setcepi  16738  resssetc  16742  resscatc  16755  catciso  16757  fthestrcsetc  16790  fullestrcsetc  16791  embedsetcestrclem  16797  fthsetcestrc  16805  fullsetcestrc  16806  evlfcl  16862  uncfcurf  16879  hofcl  16899  yonedalem3  16920  yonedainv  16921  yonffthlem  16922  yoniso  16925  isdrs2  16939  isposd  16955  pospropd  17134  poslubmo  17146  posglbmo  17147  mgmplusf  17251  issstrmgm  17252  opifismgm  17258  ismndd  17313  mndpropd  17316  issubmnd  17318  mhmpropd  17341  idmhm  17344  mhmf1o  17345  issubmd  17349  0mhm  17358  resmhm  17359  resmhm2  17360  resmhm2b  17361  mhmco  17362  submacs  17365  prdspjmhm  17367  pwsdiagmhm  17369  pwsco1mhm  17370  pwsco2mhm  17371  gsumwspan  17383  frmdsssubm  17398  frmdup1  17401  grpsubf  17494  dfgrp3  17514  mhmmnd  17537  mhmfmhm  17538  issubg4  17613  grpissubg  17614  isnsg3  17628  nsgacs  17630  0nsg  17639  nsgid  17640  isghmd  17669  ghmmhm  17670  idghm  17675  ghmnsgima  17684  ghmnsgpreima  17685  ghmf1  17689  ghmf1o  17690  gaid  17732  subgga  17733  gass  17734  gasubg  17735  cntzsubm  17768  cntrsubgnsg  17773  lactghmga  17824  symgfixf1  17857  odf1  17979  sylow1lem2  18014  sylow2blem2  18036  sylow3lem1  18042  lsmssv  18058  lsmidm  18077  pj1eu  18109  efglem  18129  efgtf  18135  efgred  18161  efgredeu  18165  frgpmhm  18178  frgpuptf  18183  frgpuplem  18185  mulgmhm  18233  ghmcmn  18237  invghm  18239  ablnsg  18250  gsum2d2lem  18372  gsum2d2  18373  gsumcom2  18374  dprd2d2  18443  ablfaclem2  18485  srgfcl  18515  srglmhm  18535  srgrmhm  18536  isrhm2d  18728  kerf1hrm  18743  issubrg2  18800  subrgint  18802  islmodd  18869  lmodscaf  18885  lmodprop2d  18925  islssd  18936  islss4  18962  lssacs  18967  lsspropd  19017  islmhmd  19039  lmhmima  19047  lmhmpreima  19048  reslmhm  19052  lspextmo  19056  lsmcl  19083  pj1lmhm  19100  islbs2  19154  issubrngd2  19189  opprdomn  19301  abvn0b  19302  issubassa2  19345  mvrf1  19425  mplsubglem  19434  mplsubrg  19440  mplcoe5lem  19467  mplcoe2  19469  mplind  19502  evlslem2  19512  evlseu  19516  ply1sclf1  19659  expmhm  19815  nn0srg  19816  prmirredlem  19841  expghm  19844  mulgghm2  19845  domnchr  19880  znf1o  19900  zntoslem  19905  znfld  19909  cygznlem3  19918  phlipf  19997  dsmmlss  20088  uvcf1  20131  frlmlbs  20136  lindff1  20159  lindfrn  20160  f1lindf  20161  mamucl  20207  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  matbas2d  20229  mamumat1cl  20245  mamulid  20247  mamurid  20248  mat1mhm  20290  dmatid  20301  dmatsubcl  20304  dmatsgrp  20305  dmatmulcl  20306  dmatsrng  20307  dmatcrng  20308  scmatscmiddistr  20314  scmatscm  20319  scmatsgrp  20325  scmatsrng  20326  scmatcrng  20327  scmatsgrp1  20328  scmatsrng1  20329  scmatf1  20337  scmatmhm  20340  mavmul0g  20359  mdet1  20407  mdetunilem9  20426  mdetuni0  20427  mdetmul  20429  madutpos  20448  smadiadetlem4  20475  1elcpmat  20520  cpmatacl  20521  cpmatmcl  20524  mat2pmatf1  20534  mat2pmatmul  20536  mat2pmat1  20537  mat2pmatlin  20540  m2cpm  20546  m2cpminvid  20558  m2cpminvid2  20560  decpmatmul  20577  pmatcollpw1  20581  monmatcollpw  20584  pmatcollpw  20586  pmatcollpw3lem  20588  pmatcollpwscmatlem2  20595  pm2mpf1  20604  mp2pm2mplem4  20614  pm2mpmhmlem2  20624  chp0mat  20651  chpidmat  20652  tgclb  20774  mretopd  20896  toponmre  20897  iscldtop  20899  ordtbaslem  20992  ordtbas2  20995  cnt0  21150  haust1  21156  cnhaus  21158  isreg2  21181  dishaus  21186  ordthaus  21188  dfconn2  21222  iunconn  21231  clsconn  21233  2ndcomap  21261  dis2ndc  21263  llynlly  21280  restnlly  21285  restlly  21286  islly2  21287  llyidm  21291  nllyidm  21292  hausllycmp  21297  kgentopon  21341  txbas  21370  ptbasin2  21381  ptbasfi  21384  txcnp  21423  txcnmpt  21427  pthaus  21441  tx1stc  21453  xkococnlem  21462  xkococn  21463  cnmpt21  21474  qtoptop2  21502  qtopeu  21519  kqt0lem  21539  isr0  21540  regr1lem2  21543  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  nrmr0reg  21552  reghmph  21596  nrmhmph  21597  txswaphmeo  21608  qtophmeo  21620  fbun  21644  trfbas2  21647  isfil2  21660  infil  21667  trfil2  21691  filssufilg  21715  hausflim  21785  fclsnei  21823  fclsfnflim  21831  flimfnfcls  21832  ptcmplem1  21856  clssubg  21912  tgpconncomp  21916  qustgplem  21924  tsmsfbas  21931  utoptop  22038  iducn  22087  cstucnd  22088  isxmetd  22131  isxmet2d  22132  xmettpos  22154  prdsdsf  22172  prdsmet  22175  ressprdsds  22176  imasdsf1olem  22178  imasf1oxmet  22180  imasf1omet  22181  blfvalps  22188  xmetresbl  22242  metss2  22317  comet  22318  stdbdmet  22321  stdbdmopn  22323  methaus  22325  met2ndci  22327  metustfbas  22362  nrmmetd  22379  subgngp  22439  ngptgp  22440  sranlm  22488  nlmvscnlem1  22490  nlmvscn  22491  nrginvrcn  22496  lssnlm  22505  nghmcn  22549  qtopbaslem  22562  reconn  22631  xmetdcn2  22640  metdscn  22659  metnrm  22665  elcncf1di  22698  cncffvrn  22701  mulc1cncf  22708  cncfco  22710  reparphti  22797  isncvsngpd  22950  tchcph  23036  ipcnlem1  23044  ipcn  23045  iscfil3  23071  bcthlem5  23125  rrxmet  23191  minveclem3  23200  minveclem7  23206  ovolicc2lem4  23288  dyadmbl  23368  volcn  23374  itg1addlem1  23459  itg1addlem2  23464  itg1addlem4  23466  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  dvmptfsum  23738  c1liplem1  23759  dvgt0lem2  23766  ftc1a  23800  ply1domn  23883  ply1divmo  23895  fta1b  23929  ig1peu  23931  coeeu  23981  plydivalg  24054  aaliou2b  24096  ulmss  24151  ulmcn  24153  efif1olem4  24291  efsubm  24297  logccv  24409  logbmpt  24526  logbfval  24528  cvxcl  24711  basellem4  24810  fsumdvdscom  24911  musum  24917  dvdsmulf1o  24920  fsumdvdsmul  24921  dchrelbasd  24964  dchrmulcl  24974  dchrinv  24986  lgsqrlem2  25072  lgsdchr  25080  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  dchrisumlema  25177  dchrisumlem2  25179  chpdifbndlem2  25243  pntpbnd  25277  pntibndlem3  25281  axtgcont  25368  iscgrglt  25409  ercgrg  25412  idmot  25432  motco  25435  cnvmot  25436  motcgrg  25439  tgisline  25522  tghilberti2  25533  mirreu3  25549  mirmot  25570  ragperp  25612  foot  25614  mideu  25630  midf  25668  lmimot  25690  trgcopyeu  25698  f1otrgds  25749  f1otrg  25751  f1otrge  25752  xmstrkgc  25766  brbtwn2  25785  axlowdimlem15  25836  axcontlem2  25845  axcontlem10  25853  eengtrkg  25865  eengtrkge  25866  numedglnl  26039  usgredgreu  26110  uspgredg2vtxeu  26112  uspgredg2v  26116  usgredg2v  26119  wlkpwwlkf1ouspgr  26765  wlknwwlksninj  26775  wlkwwlkinj  26782  wwlksnextinj  26794  clwwlksf1  26917  clwlksf1clwwlk  26969  frcond4  27134  frgrncvvdeqlem8  27170  frgrncvvdeq  27173  frgrwopreglem4  27179  numclwlk1lem2f1  27227  grpoinvf  27386  nvmf  27500  vacn  27549  nmcvcn  27550  smcnlem  27552  sspg  27583  ssps  27585  sspmlem  27587  0lno  27645  blocni  27660  sspph  27710  ipblnfi  27711  minvecolem7  27739  unopf1o  28775  cnvunop  28777  unoplin  28779  counop  28780  hmopadj2  28800  hmoplin  28801  bralnfn  28807  lnopeq0i  28866  hmops  28879  hmopm  28880  hmopco  28882  lnconi  28892  cnlnadjlem2  28927  adjmul  28951  adjadd  28952  cdjreui  29291  disjxpin  29401  off2  29443  f1od2  29499  xrofsup  29533  odutos  29663  abliso  29696  archiabllem1  29747  archiabllem2  29751  suborng  29815  xrge0slmod  29844  1smat1  29870  submateq  29875  madjusmdetlem3  29895  pstmxmet  29940  ofcf  30165  ldgenpisys  30229  rossros  30243  inelcarsg  30373  sibfof  30402  sitmf  30414  hgt750lemb  30734  erdszelem4  31176  erdszelem9  31181  erdsze2lem2  31186  cnpconn  31212  pconnconn  31213  txpconn  31214  ptpconn  31215  cvxpconn  31224  cvxsconn  31225  iccllysconn  31232  cvmseu  31258  cvmliftmo  31266  cvmlift2lem5  31289  cvmlift2lem9  31293  mrsubff1  31411  elmrsubrn  31417  mrsubco  31418  msubff1  31453  mvhf1  31456  sslttr  31914  segconeu  32118  fnessref  32352  neibastop1  32354  filnetlem3  32375  onsuct0  32440  unblimceq0lem  32497  unbdqndv2  32502  knoppndv  32525  uncf  33388  fin2so  33396  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  poimirlem26  33435  heicant  33444  mblfinlem2  33447  ftc1anc  33493  sdclem1  33539  isbnd3  33583  prdsbnd  33592  ismtycnv  33601  ismtyhmeolem  33603  ismtyres  33607  bfplem1  33621  bfplem2  33622  bfp  33623  rrnmet  33628  ismrer1  33637  iccbnd  33639  grpokerinj  33692  isdrngo2  33757  rngogrphom  33770  rngohomco  33773  rngoisocnv  33780  iscringd  33797  erprt  34158  lfl0f  34356  lkrlss  34382  lshpsmreu  34396  linepsubN  35038  pmapsub  35054  lautcnv  35376  lautco  35383  idltrn  35436  cdleme50f1  35831  cdleme50laut  35835  istendod  36050  dihf11  36556  dih1dimatlem  36618  lcfl7N  36790  lcfrlem9  36839  mapd1o  36937  hdmapf1oN  37157  hgmapf1oN  37195  nacsfix  37275  rmxypairf1o  37476  wepwsolem  37612  dnnumch3  37617  fnwe2  37623  mpaaeu  37720  idomsubgmo  37776  mon1psubm  37784  deg1mhm  37785  isotone1  38346  isotone2  38347  disjxp1  39238  disjf1  39369  wessf1ornlem  39371  projf1o  39386  sumnnodd  39862  lptioo2  39863  lptioo1  39864  cncfshift  40087  cncfperiod  40092  dvnprodlem1  40161  fourierdlem42  40366  nnfoctbdjlem  40672  isomennd  40745  smflimlem6  40984  otiunsndisjX  41298  iccpartgt  41363  icceuelpart  41372  sprsymrelfolem2  41743  sprsymrelf  41745  ismgmd  41776  mgmhmpropd  41785  mgmhmf1o  41787  idmgmhm  41788  issubmgm2  41790  rabsubmgmd  41791  resmgmhm  41798  resmgmhm2  41799  resmgmhm2b  41800  mgmhmco  41801  submgmacs  41804  opmpt2ismgm  41807  mgmplusgiopALT  41830  isrnghm2d  41901  c0mgm  41909  c0mhm  41910  lidlmmgm  41925  2zlidl  41934  rnghmsscmap2  41973  rnghmsscmap  41974  rnghmsubcsetclem2  41976  rhmsscmap2  42019  rhmsscmap  42020  rhmsubcsetclem2  42022  rhmsscrnghm  42026  rhmsubcrngclem2  42028  srhmsubc  42076  fldhmsubc  42084  rhmsubc  42090  srhmsubcALTV  42094  fldhmsubcALTV  42102  rhmsubcALTV  42108  lindslinindsimp1  42246