Theorem ralrimivva 3181

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  disjord  5089  disjxiun  5097  otsndisj  5477  otiunsndisj  5478  swopo  5553  issod  5577  reuop  6261  fcof1  7245  fliftfund  7271  isof1oidb  7282  isof1oopb  7283  soisores  7285  soisoi  7286  isocnv  7288  f1oiso  7309  oveqrspc2v  7397  oprres  7538  caovclg  7562  caovcomg  7565  off  7652  coof  7658  caofidlcan  7672  caofrss  7673  caonncan  7678  dmmpog  8030  fnmpoovd  8041  fmpoco  8049  fsplitfpar  8072  poxp  8082  fvmpocurryd  8225  smo11  8308  smoiso2  8313  omsmo  8598  nnasmo  8603  coflton  8611  qsdisj2  8746  eroprf  8766  dom2lem  8943  omxpenlem  9020  xpf1o  9081  unxpdomlem3  9172  fofinf1o  9246  dffi3  9348  supmo  9369  infmo  9414  inf3lem6  9556  cantnf  9616  rankxplim  9805  fseqenlem1  9948  fodomacn  9980  iunfictbso  10038  cofsmo  10193  infpssrlem5  10231  enfin2i  10245  fin23lem23  10250  fin23lem27  10252  fin23lem28  10264  compssiso  10298  ltordlem  11676  cju  12155  axdc4uzlem  13920  seqcaopr2  13975  seqhomo  13986  wrd2ind  14660  cshf1  14747  s3sndisj  14904  s3iunsndisj  14905  climcn2  15530  addcn2  15531  mulcn2  15533  o1of2  15550  isercolllem1  15602  fsum2dlem  15707  fsumcom2  15711  fprodser  15886  fprod2dlem  15917  fprodcom2  15921  isprm6  16655  crth  16719  eulerthlem2  16723  vdwlem12  16934  cshwsdisj  17040  imasaddfnlem  17463  imasvscafn  17472  mreexexd  17585  iscatd  17610  oppccomfpropd  17664  isofn  17713  sectmon  17720  ssctr  17763  ssceq  17764  catsubcat  17777  issubc3  17787  fullsubc  17788  fullresc  17789  isfuncd  17803  idfucl  17819  cofucl  17826  funcres2b  17835  fulloppc  17862  fthoppc  17863  idffth  17873  cofull  17874  cofth  17875  ressffth  17878  setcmon  18025  setcepi  18026  resssetc  18030  resscatc  18047  catciso  18049  fthestrcsetc  18087  fullestrcsetc  18088  embedsetcestrclem  18094  fthsetcestrc  18102  fullsetcestrc  18103  evlfcl  18159  uncfcurf  18176  hofcl  18196  yonedalem3  18217  yonedainv  18218  yonffthlem  18219  yoniso  18222  isdrs2  18243  isposd  18259  pospropd  18262  poslubmo  18346  posglbmo  18347  chnpof1  18567  mgmplusf  18589  ismgmd  18591  issstrmgm  18592  opifismgm  18598  mgmhmpropd  18637  mgmhmf1o  18639  idmgmhm  18640  issubmgm2  18642  rabsubmgmd  18643  resmgmhm  18650  resmgmhm2  18651  resmgmhm2b  18652  mgmhmco  18653  submgmacs  18656  issgrpd  18669  sgrppropd  18670  ismndd  18695  mndpropd  18698  issubmnd  18700  mndinvmod  18703  ismhmd  18725  mhmpropd  18731  idmhm  18734  mhmf1o  18735  issubmd  18745  mndissubm  18746  0mhm  18758  resmhm  18759  resmhm2  18760  resmhm2b  18761  mhmco  18762  submacs  18766  prdspjmhm  18768  pwsdiagmhm  18770  pwsco1mhm  18771  pwsco2mhm  18772  gsumwspan  18785  frmdsssubm  18800  frmdup1  18803  grpsubf  18966  dfgrp3  18986  mhmmnd  19011  mhmfmhm  19012  issubg4  19092  grpissubg  19093  isnsg3  19106  nsgacs  19108  0nsg  19115  nsgid  19116  qus0subgadd  19145  cycsubmcom  19150  isghmd  19171  ghmmhm  19172  idghm  19177  ghmnsgima  19186  ghmnsgpreima  19187  ghmf1  19192  kerf1ghm  19193  ghmf1o  19194  gaid  19245  subgga  19246  gass  19247  gasubg  19248  cntzsgrpcl  19280  cntzsubm  19284  cntrsubgnsg  19289  lactghmga  19351  symgfixf1  19383  odf1  19508  sylow1lem2  19545  sylow2blem2  19567  sylow3lem1  19573  lsmssv  19589  smndlsmidm  19602  pj1eu  19642  efglem  19662  efgtf  19668  efgred  19694  efgredeu  19698  frgpmhm  19711  frgpuptf  19716  frgpuplem  19718  mulgmhm  19773  ghmcmn  19777  invghm  19779  ablnsg  19793  imasabl  19822  cygabl  19837  gsum2d2lem  19919  gsum2d2  19920  gsumcom2  19921  dprd2d2  19992  ablfaclem2  20034  srgfcl  20148  srgcom4lem  20165  srglmhm  20173  srgrmhm  20174  ringcomlem  20231  isrnghm2d  20403  c0mgm  20412  c0mhm  20413  isrhm2d  20439  subrngringnsg  20503  issubrng2  20508  subrngint  20510  issubrg2  20542  subrgint  20545  rnghmsscmap2  20579  rnghmsscmap  20580  rnghmsubcsetclem2  20582  rhmsscmap2  20608  rhmsscmap  20609  rhmsubcsetclem2  20611  rhmsscrnghm  20615  rhmsubcrngclem2  20617  srhmsubc  20630  rhmsubc  20639  fldhmsubc  20735  primefld  20755  abvn0b  20786  suborng  20826  islmodd  20834  lmodscaf  20852  lmodprop2d  20892  islssd  20903  islss4  20930  lssacs  20935  lsspropd  20986  islmhmd  21008  lmhmima  21016  lmhmpreima  21017  reslmhm  21021  lspextmo  21025  lsmcl  21052  pj1lmhm  21069  islbs2  21126  issubrgd  21158  dflidl2rng  21190  rnglidlmmgm  21217  rhmpreimaidl  21249  rngqiprnglin  21274  expmhm  21408  nn0srg  21409  prmirredlem  21444  expghm  21447  mulgghm2  21448  domnchr  21504  znf1o  21523  zntoslem  21528  znfld  21532  cygznlem3  21541  phlipf  21624  dsmmlss  21716  uvcf1  21764  frlmlbs  21769  lindff1  21792  lindfrn  21793  f1lindf  21794  issubassa2  21865  mvrf1  21958  mplsubglem  21971  mplsubrg  21977  mplcoe5lem  22011  mplcoe2  22013  mplind  22042  evlslem2  22051  evlseu  22055  mhplss  22115  ply1sclf1  22248  evls1maplmhm  22338  mamucl  22362  mamuass  22363  mamudi  22364  mamudir  22365  mamuvs1  22366  mamuvs2  22367  matbas2d  22384  mamumat1cl  22400  mamulid  22402  mamurid  22403  mat1mhm  22445  dmatid  22456  dmatsubcl  22459  dmatsgrp  22460  dmatmulcl  22461  dmatsrng  22462  dmatcrng  22463  scmatscmiddistr  22469  scmatscm  22474  scmatsgrp  22480  scmatsrng  22481  scmatcrng  22482  scmatsgrp1  22483  scmatsrng1  22484  scmatf1  22492  scmatmhm  22495  mavmul0g  22514  mdet1  22562  mdetunilem9  22581  mdetuni0  22582  mdetmul  22584  madutpos  22603  smadiadetlem4  22630  1elcpmat  22676  cpmatacl  22677  cpmatmcl  22680  mat2pmatf1  22690  mat2pmatmul  22692  mat2pmat1  22693  mat2pmatlin  22696  m2cpm  22702  m2cpminvid  22714  m2cpminvid2  22716  decpmatmul  22733  pmatcollpw1  22737  monmatcollpw  22740  pmatcollpw  22742  pmatcollpw3lem  22744  pmatcollpwscmatlem2  22751  pm2mpf1  22760  mp2pm2mplem4  22770  pm2mpmhmlem2  22780  chp0mat  22807  chpidmat  22808  tgclb  22931  mretopd  23053  toponmre  23054  iscldtop  23056  ordtbaslem  23149  ordtbas2  23152  cnt0  23307  haust1  23313  cnhaus  23315  isreg2  23338  dishaus  23343  ordthaus  23345  dfconn2  23380  iunconn  23389  clsconn  23391  2ndcomap  23419  dis2ndc  23421  llynlly  23438  restnlly  23443  restlly  23444  islly2  23445  llyidm  23449  nllyidm  23450  hausllycmp  23455  kgentopon  23499  txbas  23528  ptbasin2  23539  ptbasfi  23542  txcnp  23581  txcnmpt  23585  pthaus  23599  tx1stc  23611  xkococnlem  23620  xkococn  23621  cnmpt21  23632  qtoptop2  23660  qtopeu  23677  kqt0lem  23697  isr0  23698  regr1lem2  23701  kqreglem1  23702  kqreglem2  23703  kqnrmlem1  23704  kqnrmlem2  23705  nrmr0reg  23710  reghmph  23754  nrmhmph  23755  txswaphmeo  23766  qtophmeo  23778  fbun  23801  trfbas2  23804  isfil2  23817  infil  23824  trfil2  23848  filssufilg  23872  hausflim  23942  fclsnei  23980  fclsfnflim  23988  flimfnfcls  23989  ptcmplem1  24013  clssubg  24070  tgpconncomp  24074  qustgplem  24082  tsmsfbas  24089  utoptop  24195  iducn  24243  cstucnd  24244  isxmetd  24287  isxmet2d  24288  xmettpos  24310  prdsdsf  24328  prdsmet  24331  ressprdsds  24332  imasdsf1olem  24334  imasf1oxmet  24336  imasf1omet  24337  blfvalps  24344  xmetresbl  24398  metss2  24473  comet  24474  stdbdmet  24477  stdbdmopn  24479  methaus  24481  met2ndci  24483  metustfbas  24518  nrmmetd  24535  subgngp  24596  ngptgp  24597  sranlm  24645  nlmvscnlem1  24647  nlmvscn  24648  nrginvrcn  24653  lssnlm  24662  nghmcn  24706  qtopbaslem  24719  reconn  24790  xmetdcn2  24799  metdscn  24818  metnrm  24824  elcncf1di  24861  cncfcdm  24864  mulc1cncf  24871  cncfco  24873  reparphti  24969  reparphtiOLD  24970  isncvsngpd  25123  tcphcph  25210  ipcnlem1  25218  ipcn  25219  iscfil3  25246  bcthlem5  25301  rrxmet  25381  minveclem3  25402  minveclem7  25408  ovolicc2lem4  25494  dyadmbl  25574  volcn  25580  itg1addlem1  25666  itg1addlem2  25671  itg1addlem4  25673  mbfi1fseqlem1  25689  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  dvmptfsum  25952  c1liplem1  25974  dvgt0lem2  25981  ftc1a  26017  ply1domn  26102  ply1divmo  26114  fta1b  26150  ig1peu  26153  coeeu  26203  plydivalg  26280  aaliou2b  26322  ulmss  26379  ulmcn  26381  efif1olem4  26527  efsubm  26533  logccv  26645  logbmpt  26771  logbfval  26773  cvxcl  26968  basellem4  27067  fsumdvdscom  27168  musum  27174  mpodvdsmulf1o  27177  fsumdvdsmul  27178  dvdsmulf1o  27179  fsumdvdsmulOLD  27180  dchrelbasd  27223  dchrmulcl  27233  dchrinv  27245  lgsqrlem2  27331  lgsdchr  27339  lgseisenlem2  27360  lgsquadlem1  27364  lgsquadlem2  27365  2sqreulem4  27438  dchrisumlema  27472  dchrisumlem2  27474  chpdifbndlem2  27538  pntpbnd  27572  pntibndlem3  27576  sltsd  27781  oldbday  27914  addsprop  27989  mulcutlem  28144  divsmo  28197  om2noseqf1o  28314  om2noseqiso  28315  axtgcont  28559  tgjustc1  28565  tgjustc2  28566  iscgrglt  28604  ercgrg  28607  idmot  28627  motco  28630  cnvmot  28631  motcgrg  28634  tgisline  28717  tghilberti2  28728  mirreu3  28744  mirmot  28765  ragperp  28807  foot  28812  mideu  28828  midf  28866  lmimot  28888  trgcopyeu  28896  f1otrgds  28959  f1otrg  28961  f1otrge  28962  xmstrkgc  28976  brbtwn2  28996  axlowdimlem15  29047  axcontlem2  29056  axcontlem10  29064  eengtrkg  29077  eengtrkge  29078  numedglnl  29235  usgredgreu  29309  uspgredg2vtxeu  29311  uspgredg2v  29315  usgredg2v  29318  wlkswwlksf1o  29970  wwlksnextinj  29990  clwlkclwwlkf1  30103  clwwlkf1  30142  frcond4  30363  frgrncvvdeqlem8  30399  frgrncvvdeq  30402  frgrwopreglem4  30408  numclwwlk1lem2f1  30450  nrt2irr  30566  grpoinvf  30626  nvmf  30739  vacn  30788  nmcvcn  30789  smcnlem  30791  sspg  30822  ssps  30824  sspmlem  30826  0lno  30884  blocni  30899  ipblnfi  30949  minvecolem7  30977  unopf1o  32010  cnvunop  32012  unoplin  32014  counop  32015  hmopadj2  32035  hmoplin  32036  bralnfn  32042  lnopeq0i  32101  hmops  32114  hmopm  32115  hmopco  32117  lnconi  32127  cnlnadjlem2  32162  adjmul  32186  adjadd  32187  cdjreui  32526  disjxpin  32681  off2  32737  2ndresdju  32745  fnpreimac  32766  suppovss  32777  f1od2  32815  xrofsup  32864  s3f1  33046  ccatf1  33048  swrdf1  33055  odutos  33067  dfmgc2lem  33094  dfmgc2  33095  pwrssmgc  33099  mgcf1o  33102  mndlactf1  33125  mndractf1  33127  abliso  33135  symgcntz  33185  tocyccntz  33244  conjga  33270  fxpsubrg  33274  archiabllem1  33293  archiabllem2  33297  urpropd  33331  elrgspnlem2  33343  rlocf1  33373  rrgsubm  33384  subrdom  33385  xrge0slmod  33447  nsgmgc  33511  intlidl  33519  idlinsubrg  33530  rhmimaidl  33531  prmidl2  33540  idlmulssprm  33541  isprmidlc  33546  rhmpreimaprmidl  33550  qsidomlem1  33551  qsidomlem2  33552  ssdifidllem  33555  ssdifidlprm  33557  mxidlprm  33569  mxidlirredi  33570  ssmxidllem  33572  rsprprmprmidl  33621  rsprprmprmidlb  33622  rprmirred  33630  rprmirredb  33631  1arithufdlem4  33646  extvfvcl  33719  mplvrpmga  33728  ply1degltdimlem  33806  ply1degltdim  33807  lindsun  33809  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  lactlmhm  33818  assalactf1o  33819  minplyirred  33895  constrsdrg  33959  1smat1  33988  submateq  33993  madjusmdetlem3  34013  zart0  34063  pstmxmet  34081  ofcf  34287  ldgenpisys  34350  rossros  34364  inelcarsg  34495  sibfof  34524  sitmf  34536  hgt750lemb  34840  erdszelem4  35416  erdszelem9  35421  erdsze2lem2  35426  cnpconn  35452  pconnconn  35453  txpconn  35454  ptpconn  35455  cvxpconn  35464  cvxsconn  35465  iccllysconn  35472  cvmseu  35498  cvmliftmo  35506  cvmlift2lem5  35529  cvmlift2lem9  35533  mrsubff1  35736  elmrsubrn  35742  mrsubco  35743  msubff1  35778  mvhf1  35781  r1peuqusdeg1  35865  segconeu  36233  fnessref  36579  neibastop1  36581  filnetlem3  36602  onsuct0  36663  weiunlem  36685  unblimceq0lem  36734  unbdqndv2  36739  knoppndv  36762  irrdiff  37608  uncf  37879  fin2so  37887  lindsadd  37893  poimirlem4  37904  poimirlem13  37913  poimirlem14  37914  poimirlem26  37926  heicant  37935  mblfinlem2  37938  ftc1anc  37981  sdclem1  38023  isbnd3  38064  prdsbnd  38073  ismtycnv  38082  ismtyhmeolem  38084  ismtyres  38088  bfplem1  38102  bfplem2  38103  bfp  38104  rrnmet  38109  ismrer1  38118  iccbnd  38120  grpokerinj  38173  isdrngo2  38238  rngogrphom  38251  rngohomco  38254  rngoisocnv  38261  iscringd  38278  eqvreldisj1  39207  erprt  39278  lfl0f  39474  lkrlss  39500  lshpsmreu  39514  linepsubN  40157  pmapsub  40173  lautcnv  40495  lautco  40502  idltrn  40555  cdleme50f1  40948  cdleme50laut  40952  istendod  41167  dihf11  41672  dih1dimatlem  41734  lcfl7N  41906  lcfrlem9  41955  mapd1o  42053  hdmapf1oN  42270  hgmapf1oN  42308  fmpocos  42635  qsalrel  42640  rediveud  42842  imacrhmcl  42913  evlselv  42974  fsuppind  42977  nacsfix  43098  rmxypairf1o  43297  wepwsolem  43428  dnnumch3  43433  fnwe2  43439  mpaaeu  43536  idomsubgmo  43579  mon1psubm  43585  deg1mhm  43586  isotone1  44433  isotone2  44434  mnringmulrcld  44613  traxext  45362  disjxp1  45458  disjf1  45571  wessf1ornlem  45573  projf1o  45584  sumnnodd  46019  lptioo2  46020  lptioo1  46021  cncfshift  46261  cncfperiod  46266  dvnprodlem1  46333  fourierdlem42  46536  nnfoctbdjlem  46842  isomennd  46918  smflimlem6  47163  fsetsnf1  47441  cfsetsnfsetf1  47448  otiunsndisjX  47668  imasetpreimafvbijlemf1  47793  iccpartgt  47816  icceuelpart  47825  ichnreuop  47861  sprsymrelfolem2  47882  sprsymrelf  47884  prproropf1o  47896  reupr  47911  reuopreuprim  47915  uhgrimprop  48281  isuspgrim0lem  48282  upgrimtrls  48295  gpgprismgr4cycllem11  48494  opmpoismgm  48556  mgmplusgiopALT  48583  2zlidl  48629  rhmsubcALTV  48674  srhmsubcALTV  48714  fldhmsubcALTV  48722  lindslinindsimp1  48846  1arymaptf1  49031  2arymaptf1  49042  eqfnovd  49254  fmpodg  49257  toslat  49370  catprsc  49401  catprsc2  49402  oppcendc  49406  invfn  49418  iinfssclem2  49443  iinfssc  49445  iinfsubc  49446  discsubc  49452  nelsubclem  49455  resccatlem  49461  funchomf  49485  imasubclem2  49493  imaidfu  49498  imasubc  49539  imassc  49541  imasubc3  49544  fthcomf  49545  idfth  49546  cofidfth  49550  upeu2  49560  isnatd  49611  swapfffth  49671  diag1f1  49695  diag2f1  49697  fucoppc  49798  isthincd  49824  isthincd2  49825  oppcthinco  49827  oppcthinendcALT  49829  functhinclem4  49835  functhincfun  49837  thincfth  49840  thincciso  49841  thinccisod  49842  functermc  49896  arweuthinc  49917  arweutermc  49918  diagffth  49926  funcsn  49929  0fucterm  49931