Theorem ralrimivva 3114

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  disjord  5058  disjxiun  5067  otsndisj  5427  otiunsndisj  5428  swopo  5505  issod  5527  reuop  6185  fcof1  7139  fliftfund  7164  isof1oidb  7175  isof1oopb  7176  soisores  7178  soisoi  7179  isocnv  7181  f1oiso  7202  oveqrspc2v  7282  oprres  7418  caovclg  7442  caovcomg  7445  off  7529  caofrss  7547  caonncan  7552  dmmpog  7888  fnmpoovd  7898  fmpoco  7906  fsplitfpar  7930  poxp  7940  fvmpocurryd  8058  smo11  8166  smoiso2  8171  omsmo  8448  qsdisj2  8542  eroprf  8562  dom2lem  8735  omxpenlem  8813  xpf1o  8875  unxpdomlem3  8958  fofinf1o  9024  dffi3  9120  supmo  9141  infmo  9184  inf3lem6  9321  cantnf  9381  rankxplim  9568  fseqenlem1  9711  fodomacn  9743  iunfictbso  9801  cofsmo  9956  infpssrlem5  9994  enfin2i  10008  fin23lem23  10013  fin23lem27  10015  fin23lem28  10027  compssiso  10061  ltordlem  11430  cju  11899  axdc4uzlem  13631  seqcaopr2  13687  seqhomo  13698  wrd2ind  14364  cshf1  14451  s3sndisj  14606  s3iunsndisj  14607  climcn2  15230  addcn2  15231  mulcn2  15233  o1of2  15250  isercolllem1  15304  fsum2dlem  15410  fsumcom2  15414  fprodser  15587  fprod2dlem  15618  fprodcom2  15622  isprm6  16347  crth  16407  eulerthlem2  16411  vdwlem12  16621  cshwsdisj  16728  imasaddfnlem  17156  imasvscafn  17165  mreexexd  17274  iscatd  17299  oppccomfpropd  17355  isofn  17404  sectmon  17411  ssctr  17454  ssceq  17455  catsubcat  17470  issubc3  17480  fullsubc  17481  fullresc  17482  isfuncd  17496  idfucl  17512  cofucl  17519  funcres2b  17528  fulloppc  17554  fthoppc  17555  idffth  17565  cofull  17566  cofth  17567  ressffth  17570  setcmon  17718  setcepi  17719  resssetc  17723  resscatc  17740  catciso  17742  fthestrcsetc  17783  fullestrcsetc  17784  embedsetcestrclem  17790  fthsetcestrc  17798  fullsetcestrc  17799  evlfcl  17856  uncfcurf  17873  hofcl  17893  yonedalem3  17914  yonedainv  17915  yonffthlem  17916  yoniso  17919  isdrs2  17939  isposd  17956  pospropd  17960  poslubmo  18044  posglbmo  18045  mgmplusf  18251  issstrmgm  18252  opifismgm  18258  ismndd  18322  mndpropd  18325  issubmnd  18327  mndinvmod  18330  mhmpropd  18351  idmhm  18354  mhmf1o  18355  issubmd  18360  mndissubm  18361  0mhm  18373  resmhm  18374  resmhm2  18375  resmhm2b  18376  mhmco  18377  submacs  18380  prdspjmhm  18382  pwsdiagmhm  18384  pwsco1mhm  18385  pwsco2mhm  18386  gsumwspan  18400  frmdsssubm  18415  frmdup1  18418  grpsubf  18569  dfgrp3  18589  mhmmnd  18612  mhmfmhm  18613  issubg4  18689  grpissubg  18690  isnsg3  18703  nsgacs  18705  0nsg  18712  nsgid  18713  cycsubmcom  18738  isghmd  18758  ghmmhm  18759  idghm  18764  ghmnsgima  18773  ghmnsgpreima  18774  ghmf1  18778  ghmf1o  18779  gaid  18820  subgga  18821  gass  18822  gasubg  18823  cntzsubm  18857  cntrsubgnsg  18862  lactghmga  18928  symgfixf1  18960  odf1  19084  sylow1lem2  19119  sylow2blem2  19141  sylow3lem1  19147  lsmssv  19163  smndlsmidm  19176  lsmidmOLD  19184  pj1eu  19217  efglem  19237  efgtf  19243  efgred  19269  efgredeu  19273  frgpmhm  19286  frgpuptf  19291  frgpuplem  19293  mulgmhm  19344  ghmcmn  19348  invghm  19350  ablnsg  19363  cygabl  19406  gsum2d2lem  19489  gsum2d2  19490  gsumcom2  19491  dprd2d2  19562  ablfaclem2  19604  srgfcl  19666  srglmhm  19686  srgrmhm  19687  isrhm2d  19887  kerf1ghm  19902  issubrg2  19959  subrgint  19961  primefld  19988  islmodd  20044  lmodscaf  20060  lmodprop2d  20100  islssd  20112  islss4  20139  lssacs  20144  lsspropd  20194  islmhmd  20216  lmhmima  20224  lmhmpreima  20225  reslmhm  20229  lspextmo  20233  lsmcl  20260  pj1lmhm  20277  islbs2  20331  issubrngd2  20372  opprdomn  20485  abvn0b  20486  expmhm  20579  nn0srg  20580  prmirredlem  20606  expghm  20609  mulgghm2  20610  domnchr  20648  znf1o  20671  zntoslem  20676  znfld  20680  cygznlem3  20689  phlipf  20769  dsmmlss  20861  uvcf1  20909  frlmlbs  20914  lindff1  20937  lindfrn  20938  f1lindf  20939  issubassa2  21006  mvrf1  21104  mplsubglem  21115  mplsubrg  21121  mplcoe5lem  21150  mplcoe2  21152  mplind  21188  evlslem2  21199  evlseu  21203  mhplss  21255  ply1sclf1  21370  mamucl  21458  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  matbas2d  21480  mamumat1cl  21496  mamulid  21498  mamurid  21499  mat1mhm  21541  dmatid  21552  dmatsubcl  21555  dmatsgrp  21556  dmatmulcl  21557  dmatsrng  21558  dmatcrng  21559  scmatscmiddistr  21565  scmatscm  21570  scmatsgrp  21576  scmatsrng  21577  scmatcrng  21578  scmatsgrp1  21579  scmatsrng1  21580  scmatf1  21588  scmatmhm  21591  mavmul0g  21610  mdet1  21658  mdetunilem9  21677  mdetuni0  21678  mdetmul  21680  madutpos  21699  smadiadetlem4  21726  1elcpmat  21772  cpmatacl  21773  cpmatmcl  21776  mat2pmatf1  21786  mat2pmatmul  21788  mat2pmat1  21789  mat2pmatlin  21792  m2cpm  21798  m2cpminvid  21810  m2cpminvid2  21812  decpmatmul  21829  pmatcollpw1  21833  monmatcollpw  21836  pmatcollpw  21838  pmatcollpw3lem  21840  pmatcollpwscmatlem2  21847  pm2mpf1  21856  mp2pm2mplem4  21866  pm2mpmhmlem2  21876  chp0mat  21903  chpidmat  21904  tgclb  22028  mretopd  22151  toponmre  22152  iscldtop  22154  ordtbaslem  22247  ordtbas2  22250  cnt0  22405  haust1  22411  cnhaus  22413  isreg2  22436  dishaus  22441  ordthaus  22443  dfconn2  22478  iunconn  22487  clsconn  22489  2ndcomap  22517  dis2ndc  22519  llynlly  22536  restnlly  22541  restlly  22542  islly2  22543  llyidm  22547  nllyidm  22548  hausllycmp  22553  kgentopon  22597  txbas  22626  ptbasin2  22637  ptbasfi  22640  txcnp  22679  txcnmpt  22683  pthaus  22697  tx1stc  22709  xkococnlem  22718  xkococn  22719  cnmpt21  22730  qtoptop2  22758  qtopeu  22775  kqt0lem  22795  isr0  22796  regr1lem2  22799  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  nrmr0reg  22808  reghmph  22852  nrmhmph  22853  txswaphmeo  22864  qtophmeo  22876  fbun  22899  trfbas2  22902  isfil2  22915  infil  22922  trfil2  22946  filssufilg  22970  hausflim  23040  fclsnei  23078  fclsfnflim  23086  flimfnfcls  23087  ptcmplem1  23111  clssubg  23168  tgpconncomp  23172  qustgplem  23180  tsmsfbas  23187  utoptop  23294  iducn  23343  cstucnd  23344  isxmetd  23387  isxmet2d  23388  xmettpos  23410  prdsdsf  23428  prdsmet  23431  ressprdsds  23432  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  blfvalps  23444  xmetresbl  23498  metss2  23574  comet  23575  stdbdmet  23578  stdbdmopn  23580  methaus  23582  met2ndci  23584  metustfbas  23619  nrmmetd  23636  subgngp  23697  ngptgp  23698  sranlm  23754  nlmvscnlem1  23756  nlmvscn  23757  nrginvrcn  23762  lssnlm  23771  nghmcn  23815  qtopbaslem  23828  reconn  23897  xmetdcn2  23906  metdscn  23925  metnrm  23931  elcncf1di  23964  cncffvrn  23967  mulc1cncf  23974  cncfco  23976  reparphti  24066  isncvsngpd  24219  tcphcph  24306  ipcnlem1  24314  ipcn  24315  iscfil3  24342  bcthlem5  24397  rrxmet  24477  minveclem3  24498  minveclem7  24504  ovolicc2lem4  24589  dyadmbl  24669  volcn  24675  itg1addlem1  24761  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  dvmptfsum  25044  c1liplem1  25065  dvgt0lem2  25072  ftc1a  25106  ply1domn  25193  ply1divmo  25205  fta1b  25239  ig1peu  25241  coeeu  25291  plydivalg  25364  aaliou2b  25406  ulmss  25461  ulmcn  25463  efif1olem4  25606  efsubm  25612  logccv  25723  logbmpt  25843  logbfval  25845  cvxcl  26039  basellem4  26138  fsumdvdscom  26239  musum  26245  dvdsmulf1o  26248  fsumdvdsmul  26249  dchrelbasd  26292  dchrmulcl  26302  dchrinv  26314  lgsqrlem2  26400  lgsdchr  26408  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  2sqreulem4  26507  dchrisumlema  26541  dchrisumlem2  26543  chpdifbndlem2  26607  pntpbnd  26641  pntibndlem3  26645  axtgcont  26734  tgjustc1  26740  tgjustc2  26741  iscgrglt  26779  ercgrg  26782  idmot  26802  motco  26805  cnvmot  26806  motcgrg  26809  tgisline  26892  tghilberti2  26903  mirreu3  26919  mirmot  26940  ragperp  26982  foot  26987  mideu  27003  midf  27041  lmimot  27063  trgcopyeu  27071  f1otrgds  27134  f1otrg  27136  f1otrge  27137  xmstrkgc  27156  brbtwn2  27176  axlowdimlem15  27227  axcontlem2  27236  axcontlem10  27244  eengtrkg  27257  eengtrkge  27258  numedglnl  27417  usgredgreu  27488  uspgredg2vtxeu  27490  uspgredg2v  27494  usgredg2v  27497  wlkswwlksf1o  28145  wwlksnextinj  28165  clwlkclwwlkf1  28275  clwwlkf1  28314  frcond4  28535  frgrncvvdeqlem8  28571  frgrncvvdeq  28574  frgrwopreglem4  28580  numclwwlk1lem2f1  28622  grpoinvf  28795  nvmf  28908  vacn  28957  nmcvcn  28958  smcnlem  28960  sspg  28991  ssps  28993  sspmlem  28995  0lno  29053  blocni  29068  ipblnfi  29118  minvecolem7  29146  unopf1o  30179  cnvunop  30181  unoplin  30183  counop  30184  hmopadj2  30204  hmoplin  30205  bralnfn  30211  lnopeq0i  30270  hmops  30283  hmopm  30284  hmopco  30286  lnconi  30296  cnlnadjlem2  30331  adjmul  30355  adjadd  30356  cdjreui  30695  disjxpin  30828  off2  30879  2ndresdju  30887  fnpreimac  30910  suppovss  30919  f1od2  30958  xrofsup  30992  s3f1  31123  ccatf1  31125  swrdf1  31130  odutos  31148  dfmgc2lem  31175  dfmgc2  31176  pwrssmgc  31180  mgcf1o  31183  abliso  31207  symgcntz  31256  tocyccntz  31313  archiabllem1  31349  archiabllem2  31353  suborng  31416  xrge0slmod  31450  nsgmgc  31499  intlidl  31504  rhmpreimaidl  31505  idlinsubrg  31510  rhmimaidl  31511  prmidl2  31518  idlmulssprm  31519  isprmidlc  31525  rhmpreimaprmidl  31529  qsidomlem1  31530  qsidomlem2  31531  mxidlprm  31542  ssmxidllem  31543  lindsun  31608  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  1smat1  31656  submateq  31661  madjusmdetlem3  31681  zart0  31731  pstmxmet  31749  ofcf  31971  ldgenpisys  32034  rossros  32048  inelcarsg  32178  sibfof  32207  sitmf  32219  hgt750lemb  32536  erdszelem4  33056  erdszelem9  33061  erdsze2lem2  33066  cnpconn  33092  pconnconn  33093  txpconn  33094  ptpconn  33095  cvxpconn  33104  cvxsconn  33105  iccllysconn  33112  cvmseu  33138  cvmliftmo  33146  cvmlift2lem5  33169  cvmlift2lem9  33173  mrsubff1  33376  elmrsubrn  33382  mrsubco  33383  msubff1  33418  mvhf1  33421  nnasmo  33596  ssltd  33913  oldbday  34008  segconeu  34240  fnessref  34473  neibastop1  34475  filnetlem3  34496  onsuct0  34557  unblimceq0lem  34613  unbdqndv2  34618  knoppndv  34641  irrdiff  35424  uncf  35683  fin2so  35691  lindsadd  35697  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  poimirlem26  35730  heicant  35739  mblfinlem2  35742  ftc1anc  35785  sdclem1  35828  isbnd3  35869  prdsbnd  35878  ismtycnv  35887  ismtyhmeolem  35889  ismtyres  35893  bfplem1  35907  bfplem2  35908  bfp  35909  rrnmet  35914  ismrer1  35923  iccbnd  35925  grpokerinj  35978  isdrngo2  36043  rngogrphom  36056  rngohomco  36059  rngoisocnv  36066  iscringd  36083  erprt  36814  lfl0f  37010  lkrlss  37036  lshpsmreu  37050  linepsubN  37693  pmapsub  37709  lautcnv  38031  lautco  38038  idltrn  38091  cdleme50f1  38484  cdleme50laut  38488  istendod  38703  dihf11  39208  dih1dimatlem  39270  lcfl7N  39442  lcfrlem9  39491  mapd1o  39589  hdmapf1oN  39806  hgmapf1oN  39844  qsalrel  40141  ismhmd  40164  fsuppind  40202  sn-negex12  40319  nacsfix  40450  rmxypairf1o  40649  wepwsolem  40783  dnnumch3  40788  fnwe2  40794  mpaaeu  40891  idomsubgmo  40939  mon1psubm  40947  deg1mhm  40948  isotone1  41547  isotone2  41548  mnringmulrcld  41735  disjxp1  42506  disjf1  42609  wessf1ornlem  42611  projf1o  42625  sumnnodd  43061  lptioo2  43062  lptioo1  43063  cncfshift  43305  cncfperiod  43310  dvnprodlem1  43377  fourierdlem42  43580  nnfoctbdjlem  43883  isomennd  43959  smflimlem6  44198  fsetsnf1  44433  cfsetsnfsetf1  44440  otiunsndisjX  44658  imasetpreimafvbijlemf1  44744  iccpartgt  44767  icceuelpart  44776  ichnreuop  44812  sprsymrelfolem2  44833  sprsymrelf  44835  prproropf1o  44847  reupr  44862  reuopreuprim  44866  isomuspgrlem2c  45170  isomuspgr  45174  ismgmd  45218  mgmhmpropd  45227  mgmhmf1o  45229  idmgmhm  45230  issubmgm2  45232  rabsubmgmd  45233  resmgmhm  45240  resmgmhm2  45241  resmgmhm2b  45242  mgmhmco  45243  submgmacs  45246  opmpoismgm  45249  mgmplusgiopALT  45276  isrnghm2d  45347  c0mgm  45355  c0mhm  45356  lidlmmgm  45371  2zlidl  45380  rnghmsscmap2  45419  rnghmsscmap  45420  rnghmsubcsetclem2  45422  rhmsscmap2  45465  rhmsscmap  45466  rhmsubcsetclem2  45468  rhmsscrnghm  45472  rhmsubcrngclem2  45474  srhmsubc  45522  fldhmsubc  45530  rhmsubc  45536  srhmsubcALTV  45540  fldhmsubcALTV  45548  rhmsubcALTV  45554  lindslinindsimp1  45686  1arymaptf1  45876  2arymaptf1  45887  toslat  46156  catprsc  46182  catprsc2  46183  isthincd  46206  isthincd2  46207  functhinclem4  46213  thincfth  46217  thincciso  46218