Theorem ralrimivva 3175

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  disjord  5078  disjxiun  5086  otsndisj  5457  otiunsndisj  5458  swopo  5533  issod  5557  reuop  6240  fcof1  7221  fliftfund  7247  isof1oidb  7258  isof1oopb  7259  soisores  7261  soisoi  7262  isocnv  7264  f1oiso  7285  oveqrspc2v  7373  oprres  7514  caovclg  7538  caovcomg  7541  off  7628  coof  7634  caofidlcan  7648  caofrss  7649  caonncan  7654  dmmpog  8006  fnmpoovd  8017  fmpoco  8025  fsplitfpar  8048  poxp  8058  fvmpocurryd  8201  smo11  8284  smoiso2  8289  omsmo  8573  nnasmo  8578  coflton  8586  qsdisj2  8719  eroprf  8739  dom2lem  8914  omxpenlem  8991  xpf1o  9052  unxpdomlem3  9142  fofinf1o  9216  dffi3  9315  supmo  9336  infmo  9381  inf3lem6  9523  cantnf  9583  rankxplim  9772  fseqenlem1  9915  fodomacn  9947  iunfictbso  10005  cofsmo  10160  infpssrlem5  10198  enfin2i  10212  fin23lem23  10217  fin23lem27  10219  fin23lem28  10231  compssiso  10265  ltordlem  11642  cju  12121  axdc4uzlem  13890  seqcaopr2  13945  seqhomo  13956  wrd2ind  14630  cshf1  14717  s3sndisj  14874  s3iunsndisj  14875  climcn2  15500  addcn2  15501  mulcn2  15503  o1of2  15520  isercolllem1  15572  fsum2dlem  15677  fsumcom2  15681  fprodser  15856  fprod2dlem  15887  fprodcom2  15891  isprm6  16625  crth  16689  eulerthlem2  16693  vdwlem12  16904  cshwsdisj  17010  imasaddfnlem  17432  imasvscafn  17441  mreexexd  17554  iscatd  17579  oppccomfpropd  17633  isofn  17682  sectmon  17689  ssctr  17732  ssceq  17733  catsubcat  17746  issubc3  17756  fullsubc  17757  fullresc  17758  isfuncd  17772  idfucl  17788  cofucl  17795  funcres2b  17804  fulloppc  17831  fthoppc  17832  idffth  17842  cofull  17843  cofth  17844  ressffth  17847  setcmon  17994  setcepi  17995  resssetc  17999  resscatc  18016  catciso  18018  fthestrcsetc  18056  fullestrcsetc  18057  embedsetcestrclem  18063  fthsetcestrc  18071  fullsetcestrc  18072  evlfcl  18128  uncfcurf  18145  hofcl  18165  yonedalem3  18186  yonedainv  18187  yonffthlem  18188  yoniso  18191  isdrs2  18212  isposd  18228  pospropd  18231  poslubmo  18315  posglbmo  18316  chnpof1  18536  mgmplusf  18558  ismgmd  18560  issstrmgm  18561  opifismgm  18567  mgmhmpropd  18606  mgmhmf1o  18608  idmgmhm  18609  issubmgm2  18611  rabsubmgmd  18612  resmgmhm  18619  resmgmhm2  18620  resmgmhm2b  18621  mgmhmco  18622  submgmacs  18625  issgrpd  18638  sgrppropd  18639  ismndd  18664  mndpropd  18667  issubmnd  18669  mndinvmod  18672  ismhmd  18694  mhmpropd  18700  idmhm  18703  mhmf1o  18704  issubmd  18714  mndissubm  18715  0mhm  18727  resmhm  18728  resmhm2  18729  resmhm2b  18730  mhmco  18731  submacs  18735  prdspjmhm  18737  pwsdiagmhm  18739  pwsco1mhm  18740  pwsco2mhm  18741  gsumwspan  18754  frmdsssubm  18769  frmdup1  18772  grpsubf  18932  dfgrp3  18952  mhmmnd  18977  mhmfmhm  18978  issubg4  19058  grpissubg  19059  isnsg3  19072  nsgacs  19074  0nsg  19081  nsgid  19082  qus0subgadd  19111  cycsubmcom  19116  isghmd  19137  ghmmhm  19138  idghm  19143  ghmnsgima  19152  ghmnsgpreima  19153  ghmf1  19158  kerf1ghm  19159  ghmf1o  19160  gaid  19211  subgga  19212  gass  19213  gasubg  19214  cntzsgrpcl  19246  cntzsubm  19250  cntrsubgnsg  19255  lactghmga  19317  symgfixf1  19349  odf1  19474  sylow1lem2  19511  sylow2blem2  19533  sylow3lem1  19539  lsmssv  19555  smndlsmidm  19568  pj1eu  19608  efglem  19628  efgtf  19634  efgred  19660  efgredeu  19664  frgpmhm  19677  frgpuptf  19682  frgpuplem  19684  mulgmhm  19739  ghmcmn  19743  invghm  19745  ablnsg  19759  imasabl  19788  cygabl  19803  gsum2d2lem  19885  gsum2d2  19886  gsumcom2  19887  dprd2d2  19958  ablfaclem2  20000  srgfcl  20114  srgcom4lem  20131  srglmhm  20139  srgrmhm  20140  ringcomlem  20197  isrnghm2d  20368  c0mgm  20377  c0mhm  20378  isrhm2d  20404  subrngringnsg  20468  issubrng2  20473  subrngint  20475  issubrg2  20507  subrgint  20510  rnghmsscmap2  20544  rnghmsscmap  20545  rnghmsubcsetclem2  20547  rhmsscmap2  20573  rhmsscmap  20574  rhmsubcsetclem2  20576  rhmsscrnghm  20580  rhmsubcrngclem2  20582  srhmsubc  20595  rhmsubc  20604  fldhmsubc  20700  primefld  20720  abvn0b  20751  suborng  20791  islmodd  20799  lmodscaf  20817  lmodprop2d  20857  islssd  20868  islss4  20895  lssacs  20900  lsspropd  20951  islmhmd  20973  lmhmima  20981  lmhmpreima  20982  reslmhm  20986  lspextmo  20990  lsmcl  21017  pj1lmhm  21034  islbs2  21091  issubrgd  21123  dflidl2rng  21155  rnglidlmmgm  21182  rhmpreimaidl  21214  rngqiprnglin  21239  expmhm  21373  nn0srg  21374  prmirredlem  21409  expghm  21412  mulgghm2  21413  domnchr  21469  znf1o  21488  zntoslem  21493  znfld  21497  cygznlem3  21506  phlipf  21589  dsmmlss  21681  uvcf1  21729  frlmlbs  21734  lindff1  21757  lindfrn  21758  f1lindf  21759  issubassa2  21829  mvrf1  21923  mplsubglem  21936  mplsubrg  21942  mplcoe5lem  21974  mplcoe2  21976  mplind  22005  evlslem2  22014  evlseu  22018  mhplss  22070  ply1sclf1  22203  evls1maplmhm  22292  mamucl  22316  mamuass  22317  mamudi  22318  mamudir  22319  mamuvs1  22320  mamuvs2  22321  matbas2d  22338  mamumat1cl  22354  mamulid  22356  mamurid  22357  mat1mhm  22399  dmatid  22410  dmatsubcl  22413  dmatsgrp  22414  dmatmulcl  22415  dmatsrng  22416  dmatcrng  22417  scmatscmiddistr  22423  scmatscm  22428  scmatsgrp  22434  scmatsrng  22435  scmatcrng  22436  scmatsgrp1  22437  scmatsrng1  22438  scmatf1  22446  scmatmhm  22449  mavmul0g  22468  mdet1  22516  mdetunilem9  22535  mdetuni0  22536  mdetmul  22538  madutpos  22557  smadiadetlem4  22584  1elcpmat  22630  cpmatacl  22631  cpmatmcl  22634  mat2pmatf1  22644  mat2pmatmul  22646  mat2pmat1  22647  mat2pmatlin  22650  m2cpm  22656  m2cpminvid  22668  m2cpminvid2  22670  decpmatmul  22687  pmatcollpw1  22691  monmatcollpw  22694  pmatcollpw  22696  pmatcollpw3lem  22698  pmatcollpwscmatlem2  22705  pm2mpf1  22714  mp2pm2mplem4  22724  pm2mpmhmlem2  22734  chp0mat  22761  chpidmat  22762  tgclb  22885  mretopd  23007  toponmre  23008  iscldtop  23010  ordtbaslem  23103  ordtbas2  23106  cnt0  23261  haust1  23267  cnhaus  23269  isreg2  23292  dishaus  23297  ordthaus  23299  dfconn2  23334  iunconn  23343  clsconn  23345  2ndcomap  23373  dis2ndc  23375  llynlly  23392  restnlly  23397  restlly  23398  islly2  23399  llyidm  23403  nllyidm  23404  hausllycmp  23409  kgentopon  23453  txbas  23482  ptbasin2  23493  ptbasfi  23496  txcnp  23535  txcnmpt  23539  pthaus  23553  tx1stc  23565  xkococnlem  23574  xkococn  23575  cnmpt21  23586  qtoptop2  23614  qtopeu  23631  kqt0lem  23651  isr0  23652  regr1lem2  23655  kqreglem1  23656  kqreglem2  23657  kqnrmlem1  23658  kqnrmlem2  23659  nrmr0reg  23664  reghmph  23708  nrmhmph  23709  txswaphmeo  23720  qtophmeo  23732  fbun  23755  trfbas2  23758  isfil2  23771  infil  23778  trfil2  23802  filssufilg  23826  hausflim  23896  fclsnei  23934  fclsfnflim  23942  flimfnfcls  23943  ptcmplem1  23967  clssubg  24024  tgpconncomp  24028  qustgplem  24036  tsmsfbas  24043  utoptop  24149  iducn  24197  cstucnd  24198  isxmetd  24241  isxmet2d  24242  xmettpos  24264  prdsdsf  24282  prdsmet  24285  ressprdsds  24286  imasdsf1olem  24288  imasf1oxmet  24290  imasf1omet  24291  blfvalps  24298  xmetresbl  24352  metss2  24427  comet  24428  stdbdmet  24431  stdbdmopn  24433  methaus  24435  met2ndci  24437  metustfbas  24472  nrmmetd  24489  subgngp  24550  ngptgp  24551  sranlm  24599  nlmvscnlem1  24601  nlmvscn  24602  nrginvrcn  24607  lssnlm  24616  nghmcn  24660  qtopbaslem  24673  reconn  24744  xmetdcn2  24753  metdscn  24772  metnrm  24778  elcncf1di  24815  cncfcdm  24818  mulc1cncf  24825  cncfco  24827  reparphti  24923  reparphtiOLD  24924  isncvsngpd  25077  tcphcph  25164  ipcnlem1  25172  ipcn  25173  iscfil3  25200  bcthlem5  25255  rrxmet  25335  minveclem3  25356  minveclem7  25362  ovolicc2lem4  25448  dyadmbl  25528  volcn  25534  itg1addlem1  25620  itg1addlem2  25625  itg1addlem4  25627  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  dvmptfsum  25906  c1liplem1  25928  dvgt0lem2  25935  ftc1a  25971  ply1domn  26056  ply1divmo  26068  fta1b  26104  ig1peu  26107  coeeu  26157  plydivalg  26234  aaliou2b  26276  ulmss  26333  ulmcn  26335  efif1olem4  26481  efsubm  26487  logccv  26599  logbmpt  26725  logbfval  26727  cvxcl  26922  basellem4  27021  fsumdvdscom  27122  musum  27128  mpodvdsmulf1o  27131  fsumdvdsmul  27132  dvdsmulf1o  27133  fsumdvdsmulOLD  27134  dchrelbasd  27177  dchrmulcl  27187  dchrinv  27199  lgsqrlem2  27285  lgsdchr  27293  lgseisenlem2  27314  lgsquadlem1  27318  lgsquadlem2  27319  2sqreulem4  27392  dchrisumlema  27426  dchrisumlem2  27428  chpdifbndlem2  27492  pntpbnd  27526  pntibndlem3  27530  ssltd  27731  oldbday  27846  addsprop  27919  mulscutlem  28070  divsmo  28123  om2noseqf1o  28231  om2noseqiso  28232  axtgcont  28447  tgjustc1  28453  tgjustc2  28454  iscgrglt  28492  ercgrg  28495  idmot  28515  motco  28518  cnvmot  28519  motcgrg  28522  tgisline  28605  tghilberti2  28616  mirreu3  28632  mirmot  28653  ragperp  28695  foot  28700  mideu  28716  midf  28754  lmimot  28776  trgcopyeu  28784  f1otrgds  28847  f1otrg  28849  f1otrge  28850  xmstrkgc  28864  brbtwn2  28883  axlowdimlem15  28934  axcontlem2  28943  axcontlem10  28951  eengtrkg  28964  eengtrkge  28965  numedglnl  29122  usgredgreu  29196  uspgredg2vtxeu  29198  uspgredg2v  29202  usgredg2v  29205  wlkswwlksf1o  29857  wwlksnextinj  29877  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  32623  2ndresdju  32631  fnpreimac  32653  suppovss  32662  f1od2  32702  xrofsup  32750  s3f1  32928  ccatf1  32930  swrdf1  32937  odutos  32949  dfmgc2lem  32976  dfmgc2  32977  pwrssmgc  32981  mgcf1o  32984  mndlactf1  33007  mndractf1  33009  abliso  33017  symgcntz  33054  tocyccntz  33113  conjga  33139  fxpsubrg  33143  archiabllem1  33162  archiabllem2  33166  urpropd  33199  elrgspnlem2  33210  rlocf1  33240  rrgsubm  33250  subrdom  33251  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  mplvrpmga  33575  ply1degltdimlem  33635  ply1degltdim  33636  lindsun  33638  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  lactlmhm  33647  assalactf1o  33648  minplyirred  33724  constrsdrg  33788  1smat1  33817  submateq  33822  madjusmdetlem3  33842  zart0  33892  pstmxmet  33910  ofcf  34116  ldgenpisys  34179  rossros  34193  inelcarsg  34324  sibfof  34353  sitmf  34365  hgt750lemb  34669  erdszelem4  35238  erdszelem9  35243  erdsze2lem2  35248  cnpconn  35274  pconnconn  35275  txpconn  35276  ptpconn  35277  cvxpconn  35286  cvxsconn  35287  iccllysconn  35294  cvmseu  35320  cvmliftmo  35328  cvmlift2lem5  35351  cvmlift2lem9  35355  mrsubff1  35558  elmrsubrn  35564  mrsubco  35565  msubff1  35600  mvhf1  35603  r1peuqusdeg1  35687  segconeu  36055  fnessref  36401  neibastop1  36403  filnetlem3  36424  onsuct0  36485  weiunlem2  36507  unblimceq0lem  36550  unbdqndv2  36555  knoppndv  36578  irrdiff  37370  uncf  37638  fin2so  37646  lindsadd  37652  poimirlem4  37663  poimirlem13  37672  poimirlem14  37673  poimirlem26  37685  heicant  37694  mblfinlem2  37697  ftc1anc  37740  sdclem1  37782  isbnd3  37823  prdsbnd  37832  ismtycnv  37841  ismtyhmeolem  37843  ismtyres  37847  bfplem1  37861  bfplem2  37862  bfp  37863  rrnmet  37868  ismrer1  37877  iccbnd  37879  grpokerinj  37932  isdrngo2  37997  rngogrphom  38010  rngohomco  38013  rngoisocnv  38020  iscringd  38037  eqvreldisj1  38921  erprt  38971  lfl0f  39167  lkrlss  39193  lshpsmreu  39207  linepsubN  39850  pmapsub  39866  lautcnv  40188  lautco  40195  idltrn  40248  cdleme50f1  40641  cdleme50laut  40645  istendod  40860  dihf11  41365  dih1dimatlem  41427  lcfl7N  41599  lcfrlem9  41648  mapd1o  41746  hdmapf1oN  41963  hgmapf1oN  42001  fmpocos  42326  qsalrel  42332  rediveud  42535  imacrhmcl  42606  evlselv  42679  fsuppind  42682  nacsfix  42804  rmxypairf1o  43003  wepwsolem  43134  dnnumch3  43139  fnwe2  43145  mpaaeu  43242  idomsubgmo  43285  mon1psubm  43291  deg1mhm  43292  isotone1  44140  isotone2  44141  mnringmulrcld  44320  traxext  45069  disjxp1  45165  disjf1  45279  wessf1ornlem  45281  projf1o  45293  sumnnodd  45729  lptioo2  45730  lptioo1  45731  cncfshift  45971  cncfperiod  45976  dvnprodlem1  46043  fourierdlem42  46246  nnfoctbdjlem  46552  isomennd  46628  smflimlem6  46873  fsetsnf1  47151  cfsetsnfsetf1  47158  otiunsndisjX  47378  imasetpreimafvbijlemf1  47503  iccpartgt  47526  icceuelpart  47535  ichnreuop  47571  sprsymrelfolem2  47592  sprsymrelf  47594  prproropf1o  47606  reupr  47621  reuopreuprim  47625  uhgrimprop  47991  isuspgrim0lem  47992  upgrimtrls  48005  gpgprismgr4cycllem11  48204  opmpoismgm  48266  mgmplusgiopALT  48293  2zlidl  48339  rhmsubcALTV  48384  srhmsubcALTV  48424  fldhmsubcALTV  48432  lindslinindsimp1  48557  1arymaptf1  48742  2arymaptf1  48753  eqfnovd  48965  fmpodg  48968  toslat  49081  catprsc  49113  catprsc2  49114  oppcendc  49118  invfn  49130  iinfssclem2  49155  iinfssc  49157  iinfsubc  49158  discsubc  49164  nelsubclem  49167  resccatlem  49173  funchomf  49197  imasubclem2  49205  imaidfu  49210  imasubc  49251  imassc  49253  imasubc3  49256  fthcomf  49257  idfth  49258  cofidfth  49262  upeu2  49272  isnatd  49323  swapfffth  49383  diag1f1  49407  diag2f1  49409  fucoppc  49510  isthincd  49536  isthincd2  49537  oppcthinco  49539  oppcthinendcALT  49541  functhinclem4  49547  functhincfun  49549  thincfth  49552  thincciso  49553  thinccisod  49554  functermc  49608  arweuthinc  49629  arweutermc  49630  diagffth  49638  funcsn  49641  0fucterm  49643