Theorem ralrimivva 3206

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 417	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 3204	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3078

This theorem is referenced by:  disjord  5097  disjxiun  5105  otsndisj  5502  otiunsndisj  5503  swopo  5580  issod  5604  reuop  6294  fcof1  7285  fliftfund  7311  isof1oidb  7322  isof1oopb  7323  soisores  7325  soisoi  7326  isocnv  7328  f1oiso  7349  oveqrspc2v  7437  oprres  7578  caovclg  7602  caovcomg  7605  off  7692  coof  7698  caofidlcan  7712  caofrss  7713  caonncan  7718  dmmpog  8070  fnmpoovd  8081  fmpoco  8089  fsplitfpar  8112  poxp  8123  fvmpocurryd  8266  smo11  8350  smoiso2  8355  omsmo  8643  nnasmo  8648  coflton  8656  qsdisj2  8792  eroprf  8812  dom2lem  8988  omxpenlem  9065  xpf1o  9126  unxpdomlem3  9217  fofinf1o  9288  dffi3  9390  supmo  9411  infmo  9456  inf3lem6  9601  cantnf  9661  rankxplim  9850  fseqenlem1  10007  fodomacn  10039  iunfictbso  10097  cofsmo  10252  infpssrlem5  10290  enfin2i  10304  fin23lem23  10309  fin23lem27  10311  fin23lem28  10323  compssiso  10357  ltordlem  11738  cju  12213  axdc4uzlem  14018  seqcaopr2  14073  seqhomo  14084  wrd2ind  14759  cshf1  14846  s3sndisj  15003  s3iunsndisj  15004  climcn2  15643  addcn2  15644  mulcn2  15646  o1of2  15663  isercolllem1  15715  fsum2dlem  15820  fsumcom2  15824  fprodser  16002  fprod2dlem  16033  fprodcom2  16037  isprm6  16772  crth  16836  eulerthlem2  16840  vdwlem12  17051  cshwsdisj  17157  imasaddfnlem  17581  imasvscafn  17590  mreexexd  17703  iscatd  17728  oppccomfpropd  17782  isofn  17831  sectmon  17838  ssctr  17881  ssceq  17882  catsubcat  17895  issubc3  17905  fullsubc  17906  fullresc  17907  isfuncd  17921  idfucl  17937  cofucl  17944  funcres2b  17953  fulloppc  17980  fthoppc  17981  idffth  17991  cofull  17992  cofth  17993  ressffth  17996  setcmon  18143  setcepi  18144  resssetc  18148  resscatc  18165  catciso  18167  fthestrcsetc  18205  fullestrcsetc  18206  embedsetcestrclem  18212  fthsetcestrc  18220  fullsetcestrc  18221  evlfcl  18277  uncfcurf  18294  hofcl  18314  yonedalem3  18335  yonedainv  18336  yonffthlem  18337  yoniso  18340  isdrs2  18361  isposd  18377  pospropd  18380  poslubmo  18464  posglbmo  18465  chnpof1  18685  mgmplusf  18707  ismgmd  18709  issstrmgm  18710  opifismgm  18716  mgmhmpropd  18755  mgmhmf1o  18757  idmgmhm  18758  issubmgm2  18760  rabsubmgmd  18761  resmgmhm  18768  resmgmhm2  18769  resmgmhm2b  18770  mgmhmco  18771  submgmacs  18774  issgrpd  18787  sgrppropd  18788  ismndd  18813  mndpropd  18816  issubmnd  18818  mndinvmod  18821  ismhmd  18843  mhmpropd  18849  idmhm  18852  mhmf1o  18853  issubmd  18863  mndissubm  18864  0mhm  18877  resmhm  18878  resmhm2  18879  resmhm2b  18880  mhmco  18881  submacs  18885  prdspjmhm  18887  pwsdiagmhm  18889  pwsco1mhm  18890  pwsco2mhm  18891  gsumwspan  18904  frmdsssubm  18919  frmdup1  18922  grpsubf  19084  dfgrp3  19104  mhmmnd  19129  mhmfmhm  19130  issubg4  19211  grpissubg  19212  isnsg3  19225  nsgacs  19227  0nsg  19234  nsgid  19235  qus0subgadd  19269  cycsubmcom  19274  isghmd  19294  ghmmhm  19295  idghm  19300  ghmnsgima  19309  ghmnsgpreima  19310  ghmf1  19315  kerf1ghm  19316  ghmf1o  19317  gaid  19368  subgga  19369  gass  19370  gasubg  19371  cntzsgrpcl  19403  cntzsubm  19407  cntrsubgnsg  19412  lactghmga  19474  symgfixf1  19506  odf1  19631  sylow1lem2  19668  sylow2blem2  19690  sylow3lem1  19696  lsmssv  19712  smndlsmidm  19725  pj1eu  19765  efglem  19785  efgtf  19791  efgred  19817  efgredeu  19821  frgpmhm  19834  frgpuptf  19839  frgpuplem  19841  mulgmhm  19896  ghmcmn  19900  invghm  19902  ablnsg  19916  imasabl  19945  cygabl  19960  gsum2d2lem  20042  gsum2d2  20043  gsumcom2  20044  dprd2d2  20115  ablfaclem2  20157  srgfcl  20277  srgcom4lem  20294  srglmhm  20302  srgrmhm  20303  ringcomlem  20361  isrnghm2d  20531  c0mgm  20540  c0mhm  20541  isrhm2d  20568  subrngringnsg  20637  issubrng2  20642  subrngint  20644  issubrg2  20676  subrgint  20679  rnghmsscmap2  20713  rnghmsscmap  20714  rnghmsubcsetclem2  20716  rhmsscmap2  20742  rhmsscmap  20743  rhmsubcsetclem2  20745  rhmsscrnghm  20749  rhmsubcrngclem2  20751  srhmsubc  20764  rhmsubc  20773  fldhmsubc  20867  primefld  20887  abvn0b  20918  suborng  20958  islmodd  20966  lmodscaf  20984  lmodprop2d  21024  islssd  21035  islss4  21062  lssacs  21067  lsspropd  21117  islmhmd  21139  lmhmima  21147  lmhmpreima  21148  reslmhm  21152  lspextmo  21156  lsmcl  21183  pj1lmhm  21200  islbs2  21257  issubrgd  21289  dflidl2rng  21322  rnglidlmmgm  21358  rhmpreimaidl  21395  rngqiprnglin  21421  prmidl2  21445  idlmulssprm  21446  isprmidlc  21451  rhmpreimaprmidl  21458  qsidomlem1  21459  qsidomlem2  21460  ssdifidllem  21463  ssdifidlprm  21465  prmidlsubm  21466  expmhm  21565  nn0srg  21566  prmirredlem  21601  expghm  21604  mulgghm2  21605  domnchr  21661  znf1o  21680  zntoslem  21685  znfld  21689  cygznlem3  21698  phlipf  21781  dsmmlss  21873  uvcf1  21921  frlmlbs  21926  lindff1  21949  lindfrn  21950  f1lindf  21951  issubassa2  22021  mvrf1  22114  mplsubglem  22127  mplsubrg  22133  mplcoe5lem  22169  mplcoe2  22171  mplind  22200  evlslem2  22209  evlseu  22213  mhplss  22297  ply1sclf1  22429  evls1maplmhm  22516  mamucl  22537  mamuass  22538  mamudi  22539  mamudir  22540  mamuvs1  22541  mamuvs2  22542  matbas2d  22559  mamumat1cl  22575  mamulid  22577  mamurid  22578  mat1mhm  22620  dmatid  22631  dmatsubcl  22634  dmatsgrp  22635  dmatmulcl  22636  dmatsrng  22637  dmatcrng  22638  scmatscmiddistr  22644  scmatscm  22649  scmatsgrp  22655  scmatsrng  22656  scmatcrng  22657  scmatsgrp1  22658  scmatsrng1  22659  scmatf1  22667  scmatmhm  22670  mavmul0g  22689  mdet1  22737  mdetunilem9  22756  mdetuni0  22757  mdetmul  22759  madutpos  22778  smadiadetlem4  22805  1elcpmat  22851  cpmatacl  22852  cpmatmcl  22855  mat2pmatf1  22865  mat2pmatmul  22867  mat2pmat1  22868  mat2pmatlin  22871  m2cpm  22877  m2cpminvid  22889  m2cpminvid2  22891  decpmatmul  22908  pmatcollpw1  22912  monmatcollpw  22915  pmatcollpw  22917  pmatcollpw3lem  22919  pmatcollpwscmatlem2  22926  pm2mpf1  22935  mp2pm2mplem4  22945  pm2mpmhmlem2  22955  chp0mat  22982  chpidmat  22983  tgclb  23106  mretopd  23228  toponmre  23229  iscldtop  23231  ordtbaslem  23324  ordtbas2  23327  cnt0  23482  haust1  23488  cnhaus  23490  isreg2  23513  dishaus  23518  ordthaus  23520  dfconn2  23555  iunconn  23564  clsconn  23566  2ndcomap  23594  dis2ndc  23596  llynlly  23613  restnlly  23618  restlly  23619  islly2  23620  llyidm  23624  nllyidm  23625  hausllycmp  23630  kgentopon  23674  txbas  23703  ptbasin2  23714  ptbasfi  23717  txcnp  23756  txcnmpt  23760  pthaus  23774  tx1stc  23786  xkococnlem  23795  xkococn  23796  cnmpt21  23807  qtoptop2  23835  qtopeu  23852  kqt0lem  23872  isr0  23873  regr1lem2  23876  kqreglem1  23877  kqreglem2  23878  kqnrmlem1  23879  kqnrmlem2  23880  nrmr0reg  23885  reghmph  23929  nrmhmph  23930  txswaphmeo  23941  qtophmeo  23953  fbun  23976  trfbas2  23979  isfil2  23992  infil  23999  trfil2  24023  filssufilg  24047  hausflim  24117  fclsnei  24155  fclsfnflim  24163  flimfnfcls  24164  ptcmplem1  24188  clssubg  24245  tgpconncomp  24249  qustgplem  24257  tsmsfbas  24264  utoptop  24370  iducn  24418  cstucnd  24419  isxmetd  24462  isxmet2d  24463  xmettpos  24485  prdsdsf  24503  prdsmet  24506  ressprdsds  24507  imasdsf1olem  24509  imasf1oxmet  24511  imasf1omet  24512  blfvalps  24519  xmetresbl  24573  metss2  24648  comet  24649  stdbdmet  24652  stdbdmopn  24654  methaus  24656  met2ndci  24658  metustfbas  24693  nrmmetd  24710  subgngp  24771  ngptgp  24772  sranlm  24820  nlmvscnlem1  24822  nlmvscn  24823  nrginvrcn  24828  lssnlm  24837  nghmcn  24881  qtopbaslem  24894  reconn  24965  xmetdcn2  24974  metdscn  24993  metnrm  24999  elcncf1di  25033  cncfcdm  25036  mulc1cncf  25043  cncfco  25045  reparphti  25135  isncvsngpd  25288  tcphcph  25375  ipcnlem1  25383  ipcn  25384  iscfil3  25411  bcthlem5  25466  rrxmet  25546  minveclem3  25567  minveclem7  25573  ovolicc2lem4  25658  dyadmbl  25738  volcn  25744  itg1addlem1  25830  itg1addlem2  25835  itg1addlem4  25837  mbfi1fseqlem1  25853  mbfi1fseqlem3  25855  mbfi1fseqlem4  25856  mbfi1fseqlem5  25857  dvmptfsum  26113  c1liplem1  26134  dvgt0lem2  26141  ftc1a  26175  ply1domn  26260  ply1divmo  26272  fta1b  26308  ig1peu  26311  coeeu  26361  plydivalg  26439  aaliou2b  26481  ulmss  26536  ulmcn  26538  efif1olem4  26686  efsubm  26692  logccv  26804  logbmpt  26929  logbfval  26931  cvxcl  27125  basellem4  27224  fsumdvdscom  27325  musum  27331  mpodvdsmulf1o  27334  fsumdvdsmul  27335  dvdsmulf1o  27336  dchrelbasd  27379  dchrmulcl  27389  dchrinv  27401  lgsqrlem2  27487  lgsdchr  27495  lgseisenlem2  27516  lgsquadlem1  27520  lgsquadlem2  27521  2sqreulem4  27594  dchrisumlema  27628  dchrisumlem2  27630  chpdifbndlem2  27694  pntpbnd  27728  pntibndlem3  27732  sltsd  27937  oldbday  28070  addsprop  28145  mulcutlem  28300  divsmo  28353  om2noseqf1o  28470  om2noseqiso  28471  axtgcont  28714  tgjustc1  28720  tgjustc2  28721  iscgrglt  28759  ercgrg  28762  idmot  28782  motco  28785  cnvmot  28786  motcgrg  28789  tgisline  28876  tghilberti2  28887  mirreu3  28907  mirmot  28928  ragperp  28972  foot  28977  mideu  28994  midf  29059  lmimot  29081  trgcopyeu  29090  prlngmolem1  29175  f1otrgds  29184  f1otrg  29186  f1otrge  29187  xmstrkgc  29201  brbtwn2  29221  axlowdimlem15  29272  axcontlem2  29281  axcontlem10  29289  eengtrkg  29302  eengtrkge  29303  numedglnl  29460  usgredgreu  29534  uspgredg2vtxeu  29536  uspgredg2v  29540  usgredg2v  29543  wlkswwlksf1o  30194  wwlksnextinj  30214  clwlkclwwlkf1  30327  clwwlkf1  30366  frcond4  30587  frgrncvvdeqlem8  30623  frgrncvvdeq  30626  frgrwopreglem4  30632  numclwwlk1lem2f1  30674  nrt2irr  30790  grpoinvf  30850  nvmf  30963  vacn  31012  nmcvcn  31013  smcnlem  31015  sspg  31046  ssps  31048  sspmlem  31050  0lno  31108  blocni  31123  ipblnfi  31173  minvecolem7  31201  unopf1o  32234  cnvunop  32236  unoplin  32238  counop  32239  hmopadj2  32259  hmoplin  32260  bralnfn  32266  lnopeq0i  32325  hmops  32338  hmopm  32339  hmopco  32341  lnconi  32351  cnlnadjlem2  32386  adjmul  32410  adjadd  32411  cdjreui  32750  disjxpin  32899  off2  32952  2ndresdju  32960  fnpreimac  32981  suppovss  32992  f1od2  33030  xrofsup  33078  s3f1  33233  ccatf1  33235  swrdf1  33242  odutos  33254  dfmgc2lem  33281  dfmgc2  33282  pwrssmgc  33286  mgcf1o  33289  mndlactf1  33312  mndractf1  33314  abliso  33321  symgcntz  33371  tocyccntz  33430  conjga  33456  fxpsubrg  33460  archiabllem1  33479  archiabllem2  33483  urpropd  33516  elrgspnlem2  33529  rlocf1  33560  rrgsubm  33570  subrdom  33571  ricdomn1  33575  xrge0slmod  33634  nsgmgc  33687  intlidl  33694  idlinsubrg  33705  rhmimaidl  33706  mxidlprm  33719  mxidlirredi  33720  ssmxidllem  33722  drnglring  33748  dflringlem2  33751  rsprprmprmidl  33778  rsprprmprmidlb  33779  rprmirred  33787  rprmirredb  33788  1arithufdlem4  33803  selvply1rhmlema  33874  selvply1rhmlem1  33876  mplidomlem  33883  extvfvcl  33892  mplvrpmga  33901  ply1degltdimlem  33978  ply1degltdim  33979  lindsun  33981  fedgmullem1  33985  fedgmullem2  33986  fedgmul  33987  lactlmhm  33990  assalactf1o  33991  minplyirred  34067  constrsdrg  34131  1smat1  34160  submateq  34165  madjusmdetlem3  34185  zart0  34235  pstmxmet  34253  ofcf  34459  ldgenpisys  34522  rossros  34536  inelcarsg  34667  sibfof  34696  sitmf  34708  hgt750lemb  35009  erdszelem4  35640  erdszelem9  35645  erdsze2lem2  35650  cnpconn  35676  pconnconn  35677  txpconn  35678  ptpconn  35679  cvxpconn  35688  cvxsconn  35689  iccllysconn  35696  cvmseu  35722  cvmliftmo  35730  cvmlift2lem5  35753  cvmlift2lem9  35757  mrsubff1  35960  elmrsubrn  35966  mrsubco  35967  msubff1  36002  mvhf1  36005  r1peuqusdeg1  36089  segconeu  36457  nmulprop  36636  fnessref  36812  neibastop1  36814  filnetlem3  36835  onsuct0  36896  weiunlem  36918  mh-inf3f1  36996  unblimceq0lem  37039  unbdqndv2  37044  knoppndv  37067  irrdiff  37914  uncf  38194  fin2so  38202  lindsadd  38208  poimirlem4  38219  poimirlem13  38228  poimirlem14  38229  poimirlem26  38241  heicant  38250  mblfinlem2  38253  ftc1anc  38296  sdclem1  38338  isbnd3  38379  prdsbnd  38388  ismtycnv  38397  ismtyhmeolem  38399  ismtyres  38403  bfplem1  38417  bfplem2  38418  bfp  38419  rrnmet  38424  ismrer1  38433  iccbnd  38435  grpokerinj  38488  isdrngo2  38553  rngogrphom  38566  rngohomco  38569  rngoisocnv  38576  iscringd  38593  eqvreldisj1  39522  erprt  39593  lfl0f  39789  lkrlss  39815  lshpsmreu  39829  linepsubN  40472  pmapsub  40488  lautcnv  40810  lautco  40817  idltrn  40870  cdleme50f1  41263  cdleme50laut  41267  istendod  41482  dihf11  41987  dih1dimatlem  42049  lcfl7N  42221  lcfrlem9  42270  mapd1o  42368  hdmapf1oN  42585  hgmapf1oN  42623  fmpocos  42950  qsalrel  42955  rediveud  43150  imacrhmcl  43234  evlselv  43269  fsuppind  43270  nacsfix  43391  rmxypairf1o  43586  wepwsolem  43717  dnnumch3  43722  fnwe2  43728  mpaaeu  43825  idomsubgmo  43868  mon1psubm  43874  deg1mhm  43875  isotone1  44722  isotone2  44723  mnringmulrcld  44900  traxext  45634  disjxp1  45737  disjf1  45849  wessf1ornlem  45851  projf1o  45862  sumnnodd  46294  lptioo2  46295  lptioo1  46296  cncfshift  46536  cncfperiod  46541  dvnprodlem1  46608  fourierdlem42  46811  nnfoctbdjlem  47117  isomennd  47193  smflimlem6  47438  fsetsnf1  47734  cfsetsnfsetf1  47741  otiunsndisjX  47961  imasetpreimafvbijlemf1  48098  iccpartgt  48121  icceuelpart  48130  ichnreuop  48166  sprsymrelfolem2  48187  sprsymrelf  48189  prproropf1o  48201  reupr  48216  reuopreuprim  48220  uhgrimprop  48602  isuspgrim0lem  48603  upgrimtrls  48616  gpgprismgr4cycllem11  48815  opmpoismgm  48877  mgmplusgiopALT  48904  2zlidl  48950  rhmsubcALTV  48995  srhmsubcALTV  49035  fldhmsubcALTV  49043  lindslinindsimp1  49182  1arymaptf1  49367  2arymaptf1  49378  eqfnovd  49589  fmpodg  49592  toslat  49705  catprsc  49736  catprsc2  49737  oppcendc  49741  invfn  49753  iinfssclem2  49778  iinfssc  49780  iinfsubc  49781  discsubc  49787  nelsubclem  49790  resccatlem  49796  funchomf  49820  imasubclem2  49828  imaidfu  49833  imasubc  49874  imassc  49876  imasubc3  49879  fthcomf  49880  idfth  49881  cofidfth  49885  upeu2  49895  isnatd  49946  swapfffth  50006  diag1f1  50030  diag2f1  50032  fucoppc  50133  isthincd  50159  isthincd2  50160  oppcthinco  50162  oppcthinendcALT  50164  functhinclem4  50170  functhincfun  50172  thincfth  50175  thincciso  50176  thinccisod  50177  functermc  50231  arweuthinc  50252  arweutermc  50253  diagffth  50261  funcsn  50264  0fucterm  50266