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 2114  ∀wral 3049

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 3050

This theorem is referenced by:  disjord  5063  disjxiun  5071  otsndisj  5462  otiunsndisj  5463  swopo  5539  issod  5563  reuop  6246  fcof1  7231  fliftfund  7257  isof1oidb  7268  isof1oopb  7269  soisores  7271  soisoi  7272  isocnv  7274  f1oiso  7295  oveqrspc2v  7383  oprres  7524  caovclg  7548  caovcomg  7551  off  7638  coof  7644  caofidlcan  7658  caofrss  7659  caonncan  7664  dmmpog  8016  fnmpoovd  8026  fmpoco  8034  fsplitfpar  8057  poxp  8067  fvmpocurryd  8210  smo11  8293  smoiso2  8298  omsmo  8583  nnasmo  8588  coflton  8596  qsdisj2  8731  eroprf  8751  dom2lem  8928  omxpenlem  9005  xpf1o  9066  unxpdomlem3  9157  fofinf1o  9231  dffi3  9333  supmo  9354  infmo  9399  inf3lem6  9543  cantnf  9603  rankxplim  9792  fseqenlem1  9935  fodomacn  9967  iunfictbso  10025  cofsmo  10180  infpssrlem5  10218  enfin2i  10232  fin23lem23  10237  fin23lem27  10239  fin23lem28  10251  compssiso  10285  ltordlem  11664  cju  12144  axdc4uzlem  13934  seqcaopr2  13989  seqhomo  14000  wrd2ind  14674  cshf1  14761  s3sndisj  14918  s3iunsndisj  14919  climcn2  15544  addcn2  15545  mulcn2  15547  o1of2  15564  isercolllem1  15616  fsum2dlem  15721  fsumcom2  15725  fprodser  15903  fprod2dlem  15934  fprodcom2  15938  isprm6  16673  crth  16737  eulerthlem2  16741  vdwlem12  16952  cshwsdisj  17058  imasaddfnlem  17481  imasvscafn  17490  mreexexd  17603  iscatd  17628  oppccomfpropd  17682  isofn  17731  sectmon  17738  ssctr  17781  ssceq  17782  catsubcat  17795  issubc3  17805  fullsubc  17806  fullresc  17807  isfuncd  17821  idfucl  17837  cofucl  17844  funcres2b  17853  fulloppc  17880  fthoppc  17881  idffth  17891  cofull  17892  cofth  17893  ressffth  17896  setcmon  18043  setcepi  18044  resssetc  18048  resscatc  18065  catciso  18067  fthestrcsetc  18105  fullestrcsetc  18106  embedsetcestrclem  18112  fthsetcestrc  18120  fullsetcestrc  18121  evlfcl  18177  uncfcurf  18194  hofcl  18214  yonedalem3  18235  yonedainv  18236  yonffthlem  18237  yoniso  18240  isdrs2  18261  isposd  18277  pospropd  18280  poslubmo  18364  posglbmo  18365  chnpof1  18585  mgmplusf  18607  ismgmd  18609  issstrmgm  18610  opifismgm  18616  mgmhmpropd  18655  mgmhmf1o  18657  idmgmhm  18658  issubmgm2  18660  rabsubmgmd  18661  resmgmhm  18668  resmgmhm2  18669  resmgmhm2b  18670  mgmhmco  18671  submgmacs  18674  issgrpd  18687  sgrppropd  18688  ismndd  18713  mndpropd  18716  issubmnd  18718  mndinvmod  18721  ismhmd  18743  mhmpropd  18749  idmhm  18752  mhmf1o  18753  issubmd  18763  mndissubm  18764  0mhm  18776  resmhm  18777  resmhm2  18778  resmhm2b  18779  mhmco  18780  submacs  18784  prdspjmhm  18786  pwsdiagmhm  18788  pwsco1mhm  18789  pwsco2mhm  18790  gsumwspan  18803  frmdsssubm  18818  frmdup1  18821  grpsubf  18984  dfgrp3  19004  mhmmnd  19029  mhmfmhm  19030  issubg4  19110  grpissubg  19111  isnsg3  19124  nsgacs  19126  0nsg  19133  nsgid  19134  qus0subgadd  19163  cycsubmcom  19168  isghmd  19189  ghmmhm  19190  idghm  19195  ghmnsgima  19204  ghmnsgpreima  19205  ghmf1  19210  kerf1ghm  19211  ghmf1o  19212  gaid  19263  subgga  19264  gass  19265  gasubg  19266  cntzsgrpcl  19298  cntzsubm  19302  cntrsubgnsg  19307  lactghmga  19369  symgfixf1  19401  odf1  19526  sylow1lem2  19563  sylow2blem2  19585  sylow3lem1  19591  lsmssv  19607  smndlsmidm  19620  pj1eu  19660  efglem  19680  efgtf  19686  efgred  19712  efgredeu  19716  frgpmhm  19729  frgpuptf  19734  frgpuplem  19736  mulgmhm  19791  ghmcmn  19795  invghm  19797  ablnsg  19811  imasabl  19840  cygabl  19855  gsum2d2lem  19937  gsum2d2  19938  gsumcom2  19939  dprd2d2  20010  ablfaclem2  20052  srgfcl  20166  srgcom4lem  20183  srglmhm  20191  srgrmhm  20192  ringcomlem  20249  isrnghm2d  20419  c0mgm  20428  c0mhm  20429  isrhm2d  20455  subrngringnsg  20519  issubrng2  20524  subrngint  20526  issubrg2  20558  subrgint  20561  rnghmsscmap2  20595  rnghmsscmap  20596  rnghmsubcsetclem2  20598  rhmsscmap2  20624  rhmsscmap  20625  rhmsubcsetclem2  20627  rhmsscrnghm  20631  rhmsubcrngclem2  20633  srhmsubc  20646  rhmsubc  20655  fldhmsubc  20751  primefld  20771  abvn0b  20802  suborng  20842  islmodd  20850  lmodscaf  20868  lmodprop2d  20908  islssd  20919  islss4  20946  lssacs  20951  lsspropd  21001  islmhmd  21023  lmhmima  21031  lmhmpreima  21032  reslmhm  21036  lspextmo  21040  lsmcl  21067  pj1lmhm  21084  islbs2  21141  issubrgd  21173  dflidl2rng  21205  rnglidlmmgm  21232  rhmpreimaidl  21264  rngqiprnglin  21289  expmhm  21405  nn0srg  21406  prmirredlem  21441  expghm  21444  mulgghm2  21445  domnchr  21501  znf1o  21520  zntoslem  21525  znfld  21529  cygznlem3  21538  phlipf  21621  dsmmlss  21713  uvcf1  21761  frlmlbs  21766  lindff1  21789  lindfrn  21790  f1lindf  21791  issubassa2  21861  mvrf1  21953  mplsubglem  21966  mplsubrg  21972  mplcoe5lem  22006  mplcoe2  22008  mplind  22037  evlslem2  22046  evlseu  22050  mhplss  22110  ply1sclf1  22242  evls1maplmhm  22330  mamucl  22354  mamuass  22355  mamudi  22356  mamudir  22357  mamuvs1  22358  mamuvs2  22359  matbas2d  22376  mamumat1cl  22392  mamulid  22394  mamurid  22395  mat1mhm  22437  dmatid  22448  dmatsubcl  22451  dmatsgrp  22452  dmatmulcl  22453  dmatsrng  22454  dmatcrng  22455  scmatscmiddistr  22461  scmatscm  22466  scmatsgrp  22472  scmatsrng  22473  scmatcrng  22474  scmatsgrp1  22475  scmatsrng1  22476  scmatf1  22484  scmatmhm  22487  mavmul0g  22506  mdet1  22554  mdetunilem9  22573  mdetuni0  22574  mdetmul  22576  madutpos  22595  smadiadetlem4  22622  1elcpmat  22668  cpmatacl  22669  cpmatmcl  22672  mat2pmatf1  22682  mat2pmatmul  22684  mat2pmat1  22685  mat2pmatlin  22688  m2cpm  22694  m2cpminvid  22706  m2cpminvid2  22708  decpmatmul  22725  pmatcollpw1  22729  monmatcollpw  22732  pmatcollpw  22734  pmatcollpw3lem  22736  pmatcollpwscmatlem2  22743  pm2mpf1  22752  mp2pm2mplem4  22762  pm2mpmhmlem2  22772  chp0mat  22799  chpidmat  22800  tgclb  22923  mretopd  23045  toponmre  23046  iscldtop  23048  ordtbaslem  23141  ordtbas2  23144  cnt0  23299  haust1  23305  cnhaus  23307  isreg2  23330  dishaus  23335  ordthaus  23337  dfconn2  23372  iunconn  23381  clsconn  23383  2ndcomap  23411  dis2ndc  23413  llynlly  23430  restnlly  23435  restlly  23436  islly2  23437  llyidm  23441  nllyidm  23442  hausllycmp  23447  kgentopon  23491  txbas  23520  ptbasin2  23531  ptbasfi  23534  txcnp  23573  txcnmpt  23577  pthaus  23591  tx1stc  23603  xkococnlem  23612  xkococn  23613  cnmpt21  23624  qtoptop2  23652  qtopeu  23669  kqt0lem  23689  isr0  23690  regr1lem2  23693  kqreglem1  23694  kqreglem2  23695  kqnrmlem1  23696  kqnrmlem2  23697  nrmr0reg  23702  reghmph  23746  nrmhmph  23747  txswaphmeo  23758  qtophmeo  23770  fbun  23793  trfbas2  23796  isfil2  23809  infil  23816  trfil2  23840  filssufilg  23864  hausflim  23934  fclsnei  23972  fclsfnflim  23980  flimfnfcls  23981  ptcmplem1  24005  clssubg  24062  tgpconncomp  24066  qustgplem  24074  tsmsfbas  24081  utoptop  24187  iducn  24235  cstucnd  24236  isxmetd  24279  isxmet2d  24280  xmettpos  24302  prdsdsf  24320  prdsmet  24323  ressprdsds  24324  imasdsf1olem  24326  imasf1oxmet  24328  imasf1omet  24329  blfvalps  24336  xmetresbl  24390  metss2  24465  comet  24466  stdbdmet  24469  stdbdmopn  24471  methaus  24473  met2ndci  24475  metustfbas  24510  nrmmetd  24527  subgngp  24588  ngptgp  24589  sranlm  24637  nlmvscnlem1  24639  nlmvscn  24640  nrginvrcn  24645  lssnlm  24654  nghmcn  24698  qtopbaslem  24711  reconn  24782  xmetdcn2  24791  metdscn  24810  metnrm  24816  elcncf1di  24850  cncfcdm  24853  mulc1cncf  24860  cncfco  24862  reparphti  24952  isncvsngpd  25105  tcphcph  25192  ipcnlem1  25200  ipcn  25201  iscfil3  25228  bcthlem5  25283  rrxmet  25363  minveclem3  25384  minveclem7  25390  ovolicc2lem4  25475  dyadmbl  25555  volcn  25561  itg1addlem1  25647  itg1addlem2  25652  itg1addlem4  25654  mbfi1fseqlem1  25670  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  dvmptfsum  25930  c1liplem1  25951  dvgt0lem2  25958  ftc1a  25992  ply1domn  26077  ply1divmo  26089  fta1b  26125  ig1peu  26128  coeeu  26178  plydivalg  26253  aaliou2b  26295  ulmss  26350  ulmcn  26352  efif1olem4  26497  efsubm  26503  logccv  26615  logbmpt  26740  logbfval  26742  cvxcl  26936  basellem4  27035  fsumdvdscom  27136  musum  27142  mpodvdsmulf1o  27145  fsumdvdsmul  27146  dvdsmulf1o  27147  dchrelbasd  27190  dchrmulcl  27200  dchrinv  27212  lgsqrlem2  27298  lgsdchr  27306  lgseisenlem2  27327  lgsquadlem1  27331  lgsquadlem2  27332  2sqreulem4  27405  dchrisumlema  27439  dchrisumlem2  27441  chpdifbndlem2  27505  pntpbnd  27539  pntibndlem3  27543  sltsd  27748  oldbday  27881  addsprop  27956  mulcutlem  28111  divsmo  28164  om2noseqf1o  28281  om2noseqiso  28282  axtgcont  28525  tgjustc1  28531  tgjustc2  28532  iscgrglt  28570  ercgrg  28573  idmot  28593  motco  28596  cnvmot  28597  motcgrg  28600  tgisline  28683  tghilberti2  28694  mirreu3  28710  mirmot  28731  ragperp  28773  foot  28778  mideu  28794  midf  28832  lmimot  28854  trgcopyeu  28862  f1otrgds  28925  f1otrg  28927  f1otrge  28928  xmstrkgc  28942  brbtwn2  28962  axlowdimlem15  29013  axcontlem2  29022  axcontlem10  29030  eengtrkg  29043  eengtrkge  29044  numedglnl  29201  usgredgreu  29275  uspgredg2vtxeu  29277  uspgredg2v  29281  usgredg2v  29284  wlkswwlksf1o  29935  wwlksnextinj  29955  clwlkclwwlkf1  30068  clwwlkf1  30107  frcond4  30328  frgrncvvdeqlem8  30364  frgrncvvdeq  30367  frgrwopreglem4  30373  numclwwlk1lem2f1  30415  nrt2irr  30531  grpoinvf  30591  nvmf  30704  vacn  30753  nmcvcn  30754  smcnlem  30756  sspg  30787  ssps  30789  sspmlem  30791  0lno  30849  blocni  30864  ipblnfi  30914  minvecolem7  30942  unopf1o  31975  cnvunop  31977  unoplin  31979  counop  31980  hmopadj2  32000  hmoplin  32001  bralnfn  32007  lnopeq0i  32066  hmops  32079  hmopm  32080  hmopco  32082  lnconi  32092  cnlnadjlem2  32127  adjmul  32151  adjadd  32152  cdjreui  32491  disjxpin  32646  off2  32702  2ndresdju  32710  fnpreimac  32731  suppovss  32742  f1od2  32780  xrofsup  32828  s3f1  32995  ccatf1  32997  swrdf1  33004  odutos  33016  dfmgc2lem  33043  dfmgc2  33044  pwrssmgc  33048  mgcf1o  33051  mndlactf1  33074  mndractf1  33076  abliso  33084  symgcntz  33134  tocyccntz  33193  conjga  33219  fxpsubrg  33223  archiabllem1  33242  archiabllem2  33246  urpropd  33280  elrgspnlem2  33292  rlocf1  33322  rrgsubm  33333  subrdom  33334  xrge0slmod  33396  nsgmgc  33460  intlidl  33468  idlinsubrg  33479  rhmimaidl  33480  prmidl2  33489  idlmulssprm  33490  isprmidlc  33495  rhmpreimaprmidl  33499  qsidomlem1  33500  qsidomlem2  33501  ssdifidllem  33504  ssdifidlprm  33506  mxidlprm  33518  mxidlirredi  33519  ssmxidllem  33521  rsprprmprmidl  33570  rsprprmprmidlb  33571  rprmirred  33579  rprmirredb  33580  1arithufdlem4  33595  extvfvcl  33668  mplvrpmga  33677  ply1degltdimlem  33754  ply1degltdim  33755  lindsun  33757  fedgmullem1  33761  fedgmullem2  33762  fedgmul  33763  lactlmhm  33766  assalactf1o  33767  minplyirred  33843  constrsdrg  33907  1smat1  33936  submateq  33941  madjusmdetlem3  33961  zart0  34011  pstmxmet  34029  ofcf  34235  ldgenpisys  34298  rossros  34312  inelcarsg  34443  sibfof  34472  sitmf  34484  hgt750lemb  34788  erdszelem4  35364  erdszelem9  35369  erdsze2lem2  35374  cnpconn  35400  pconnconn  35401  txpconn  35402  ptpconn  35403  cvxpconn  35412  cvxsconn  35413  iccllysconn  35420  cvmseu  35446  cvmliftmo  35454  cvmlift2lem5  35477  cvmlift2lem9  35481  mrsubff1  35684  elmrsubrn  35690  mrsubco  35691  msubff1  35726  mvhf1  35729  r1peuqusdeg1  35813  segconeu  36181  fnessref  36527  neibastop1  36529  filnetlem3  36550  onsuct0  36611  weiunlem  36633  mh-inf3f1  36711  unblimceq0lem  36754  unbdqndv2  36759  knoppndv  36782  irrdiff  37628  uncf  37908  fin2so  37916  lindsadd  37922  poimirlem4  37933  poimirlem13  37942  poimirlem14  37943  poimirlem26  37955  heicant  37964  mblfinlem2  37967  ftc1anc  38010  sdclem1  38052  isbnd3  38093  prdsbnd  38102  ismtycnv  38111  ismtyhmeolem  38113  ismtyres  38117  bfplem1  38131  bfplem2  38132  bfp  38133  rrnmet  38138  ismrer1  38147  iccbnd  38149  grpokerinj  38202  isdrngo2  38267  rngogrphom  38280  rngohomco  38283  rngoisocnv  38290  iscringd  38307  eqvreldisj1  39236  erprt  39307  lfl0f  39503  lkrlss  39529  lshpsmreu  39543  linepsubN  40186  pmapsub  40202  lautcnv  40524  lautco  40531  idltrn  40584  cdleme50f1  40977  cdleme50laut  40981  istendod  41196  dihf11  41701  dih1dimatlem  41763  lcfl7N  41935  lcfrlem9  41984  mapd1o  42082  hdmapf1oN  42299  hgmapf1oN  42337  fmpocos  42663  qsalrel  42668  rediveud  42863  imacrhmcl  42947  evlselv  43008  fsuppind  43011  nacsfix  43132  rmxypairf1o  43327  wepwsolem  43458  dnnumch3  43463  fnwe2  43469  mpaaeu  43566  idomsubgmo  43609  mon1psubm  43615  deg1mhm  43616  isotone1  44463  isotone2  44464  mnringmulrcld  44643  traxext  45392  disjxp1  45488  disjf1  45601  wessf1ornlem  45603  projf1o  45614  sumnnodd  46048  lptioo2  46049  lptioo1  46050  cncfshift  46290  cncfperiod  46295  dvnprodlem1  46362  fourierdlem42  46565  nnfoctbdjlem  46871  isomennd  46947  smflimlem6  47192  fsetsnf1  47488  cfsetsnfsetf1  47495  otiunsndisjX  47715  imasetpreimafvbijlemf1  47852  iccpartgt  47875  icceuelpart  47884  ichnreuop  47920  sprsymrelfolem2  47941  sprsymrelf  47943  prproropf1o  47955  reupr  47970  reuopreuprim  47974  uhgrimprop  48356  isuspgrim0lem  48357  upgrimtrls  48370  gpgprismgr4cycllem11  48569  opmpoismgm  48631  mgmplusgiopALT  48658  2zlidl  48704  rhmsubcALTV  48749  srhmsubcALTV  48789  fldhmsubcALTV  48797  lindslinindsimp1  48921  1arymaptf1  49106  2arymaptf1  49117  eqfnovd  49329  fmpodg  49332  toslat  49445  catprsc  49476  catprsc2  49477  oppcendc  49481  invfn  49493  iinfssclem2  49518  iinfssc  49520  iinfsubc  49521  discsubc  49527  nelsubclem  49530  resccatlem  49536  funchomf  49560  imasubclem2  49568  imaidfu  49573  imasubc  49614  imassc  49616  imasubc3  49619  fthcomf  49620  idfth  49621  cofidfth  49625  upeu2  49635  isnatd  49686  swapfffth  49746  diag1f1  49770  diag2f1  49772  fucoppc  49873  isthincd  49899  isthincd2  49900  oppcthinco  49902  oppcthinendcALT  49904  functhinclem4  49910  functhincfun  49912  thincfth  49915  thincciso  49916  thinccisod  49917  functermc  49971  arweuthinc  49992  arweutermc  49993  diagffth  50001  funcsn  50004  0fucterm  50006