Theorem ralrimivva 3124

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3070

This theorem is referenced by:  disjord  5063  disjxiun  5072  otsndisj  5434  otiunsndisj  5435  swopo  5515  issod  5537  reuop  6200  fcof1  7168  fliftfund  7193  isof1oidb  7204  isof1oopb  7205  soisores  7207  soisoi  7208  isocnv  7210  f1oiso  7231  oveqrspc2v  7311  oprres  7449  caovclg  7473  caovcomg  7476  off  7560  caofrss  7578  caonncan  7583  dmmpog  7924  fnmpoovd  7936  fmpoco  7944  fsplitfpar  7968  poxp  7978  fvmpocurryd  8096  smo11  8204  smoiso2  8209  omsmo  8497  nnasmo  8502  qsdisj2  8593  eroprf  8613  dom2lem  8789  omxpenlem  8869  xpf1o  8935  unxpdomlem3  9038  fofinf1o  9103  dffi3  9199  supmo  9220  infmo  9263  inf3lem6  9400  cantnf  9460  rankxplim  9646  fseqenlem1  9789  fodomacn  9821  iunfictbso  9879  cofsmo  10034  infpssrlem5  10072  enfin2i  10086  fin23lem23  10091  fin23lem27  10093  fin23lem28  10105  compssiso  10139  ltordlem  11509  cju  11978  axdc4uzlem  13712  seqcaopr2  13768  seqhomo  13779  wrd2ind  14445  cshf1  14532  s3sndisj  14687  s3iunsndisj  14688  climcn2  15311  addcn2  15312  mulcn2  15314  o1of2  15331  isercolllem1  15385  fsum2dlem  15491  fsumcom2  15495  fprodser  15668  fprod2dlem  15699  fprodcom2  15703  isprm6  16428  crth  16488  eulerthlem2  16492  vdwlem12  16702  cshwsdisj  16809  imasaddfnlem  17248  imasvscafn  17257  mreexexd  17366  iscatd  17391  oppccomfpropd  17447  isofn  17496  sectmon  17503  ssctr  17546  ssceq  17547  catsubcat  17563  issubc3  17573  fullsubc  17574  fullresc  17575  isfuncd  17589  idfucl  17605  cofucl  17612  funcres2b  17621  fulloppc  17647  fthoppc  17648  idffth  17658  cofull  17659  cofth  17660  ressffth  17663  setcmon  17811  setcepi  17812  resssetc  17816  resscatc  17833  catciso  17835  fthestrcsetc  17876  fullestrcsetc  17877  embedsetcestrclem  17883  fthsetcestrc  17891  fullsetcestrc  17892  evlfcl  17949  uncfcurf  17966  hofcl  17986  yonedalem3  18007  yonedainv  18008  yonffthlem  18009  yoniso  18012  isdrs2  18033  isposd  18050  pospropd  18054  poslubmo  18138  posglbmo  18139  mgmplusf  18345  issstrmgm  18346  opifismgm  18352  ismndd  18416  mndpropd  18419  issubmnd  18421  mndinvmod  18424  mhmpropd  18445  idmhm  18448  mhmf1o  18449  issubmd  18454  mndissubm  18455  0mhm  18467  resmhm  18468  resmhm2  18469  resmhm2b  18470  mhmco  18471  submacs  18474  prdspjmhm  18476  pwsdiagmhm  18478  pwsco1mhm  18479  pwsco2mhm  18480  gsumwspan  18494  frmdsssubm  18509  frmdup1  18512  grpsubf  18663  dfgrp3  18683  mhmmnd  18706  mhmfmhm  18707  issubg4  18783  grpissubg  18784  isnsg3  18797  nsgacs  18799  0nsg  18806  nsgid  18807  cycsubmcom  18832  isghmd  18852  ghmmhm  18853  idghm  18858  ghmnsgima  18867  ghmnsgpreima  18868  ghmf1  18872  ghmf1o  18873  gaid  18914  subgga  18915  gass  18916  gasubg  18917  cntzsubm  18951  cntrsubgnsg  18956  lactghmga  19022  symgfixf1  19054  odf1  19178  sylow1lem2  19213  sylow2blem2  19235  sylow3lem1  19241  lsmssv  19257  smndlsmidm  19270  lsmidmOLD  19278  pj1eu  19311  efglem  19331  efgtf  19337  efgred  19363  efgredeu  19367  frgpmhm  19380  frgpuptf  19385  frgpuplem  19387  mulgmhm  19438  ghmcmn  19442  invghm  19444  ablnsg  19457  cygabl  19500  gsum2d2lem  19583  gsum2d2  19584  gsumcom2  19585  dprd2d2  19656  ablfaclem2  19698  srgfcl  19760  srglmhm  19780  srgrmhm  19781  isrhm2d  19981  kerf1ghm  19996  issubrg2  20053  subrgint  20055  primefld  20082  islmodd  20138  lmodscaf  20154  lmodprop2d  20194  islssd  20206  islss4  20233  lssacs  20238  lsspropd  20288  islmhmd  20310  lmhmima  20318  lmhmpreima  20319  reslmhm  20323  lspextmo  20327  lsmcl  20354  pj1lmhm  20371  islbs2  20425  issubrngd2  20468  opprdomn  20581  abvn0b  20582  expmhm  20676  nn0srg  20677  prmirredlem  20703  expghm  20706  mulgghm2  20707  domnchr  20745  znf1o  20768  zntoslem  20773  znfld  20777  cygznlem3  20786  phlipf  20866  dsmmlss  20960  uvcf1  21008  frlmlbs  21013  lindff1  21036  lindfrn  21037  f1lindf  21038  issubassa2  21105  mvrf1  21203  mplsubglem  21214  mplsubrg  21220  mplcoe5lem  21249  mplcoe2  21251  mplind  21287  evlslem2  21298  evlseu  21302  mhplss  21354  ply1sclf1  21469  mamucl  21557  mamuass  21558  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  matbas2d  21581  mamumat1cl  21597  mamulid  21599  mamurid  21600  mat1mhm  21642  dmatid  21653  dmatsubcl  21656  dmatsgrp  21657  dmatmulcl  21658  dmatsrng  21659  dmatcrng  21660  scmatscmiddistr  21666  scmatscm  21671  scmatsgrp  21677  scmatsrng  21678  scmatcrng  21679  scmatsgrp1  21680  scmatsrng1  21681  scmatf1  21689  scmatmhm  21692  mavmul0g  21711  mdet1  21759  mdetunilem9  21778  mdetuni0  21779  mdetmul  21781  madutpos  21800  smadiadetlem4  21827  1elcpmat  21873  cpmatacl  21874  cpmatmcl  21877  mat2pmatf1  21887  mat2pmatmul  21889  mat2pmat1  21890  mat2pmatlin  21893  m2cpm  21899  m2cpminvid  21911  m2cpminvid2  21913  decpmatmul  21930  pmatcollpw1  21934  monmatcollpw  21937  pmatcollpw  21939  pmatcollpw3lem  21941  pmatcollpwscmatlem2  21948  pm2mpf1  21957  mp2pm2mplem4  21967  pm2mpmhmlem2  21977  chp0mat  22004  chpidmat  22005  tgclb  22129  mretopd  22252  toponmre  22253  iscldtop  22255  ordtbaslem  22348  ordtbas2  22351  cnt0  22506  haust1  22512  cnhaus  22514  isreg2  22537  dishaus  22542  ordthaus  22544  dfconn2  22579  iunconn  22588  clsconn  22590  2ndcomap  22618  dis2ndc  22620  llynlly  22637  restnlly  22642  restlly  22643  islly2  22644  llyidm  22648  nllyidm  22649  hausllycmp  22654  kgentopon  22698  txbas  22727  ptbasin2  22738  ptbasfi  22741  txcnp  22780  txcnmpt  22784  pthaus  22798  tx1stc  22810  xkococnlem  22819  xkococn  22820  cnmpt21  22831  qtoptop2  22859  qtopeu  22876  kqt0lem  22896  isr0  22897  regr1lem2  22900  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  nrmr0reg  22909  reghmph  22953  nrmhmph  22954  txswaphmeo  22965  qtophmeo  22977  fbun  23000  trfbas2  23003  isfil2  23016  infil  23023  trfil2  23047  filssufilg  23071  hausflim  23141  fclsnei  23179  fclsfnflim  23187  flimfnfcls  23188  ptcmplem1  23212  clssubg  23269  tgpconncomp  23273  qustgplem  23281  tsmsfbas  23288  utoptop  23395  iducn  23444  cstucnd  23445  isxmetd  23488  isxmet2d  23489  xmettpos  23511  prdsdsf  23529  prdsmet  23532  ressprdsds  23533  imasdsf1olem  23535  imasf1oxmet  23537  imasf1omet  23538  blfvalps  23545  xmetresbl  23599  metss2  23677  comet  23678  stdbdmet  23681  stdbdmopn  23683  methaus  23685  met2ndci  23687  metustfbas  23722  nrmmetd  23739  subgngp  23800  ngptgp  23801  sranlm  23857  nlmvscnlem1  23859  nlmvscn  23860  nrginvrcn  23865  lssnlm  23874  nghmcn  23918  qtopbaslem  23931  reconn  24000  xmetdcn2  24009  metdscn  24028  metnrm  24034  elcncf1di  24067  cncffvrn  24070  mulc1cncf  24077  cncfco  24079  reparphti  24169  isncvsngpd  24323  tcphcph  24410  ipcnlem1  24418  ipcn  24419  iscfil3  24446  bcthlem5  24501  rrxmet  24581  minveclem3  24602  minveclem7  24608  ovolicc2lem4  24693  dyadmbl  24773  volcn  24779  itg1addlem1  24865  itg1addlem2  24870  itg1addlem4  24872  itg1addlem4OLD  24873  mbfi1fseqlem1  24889  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  dvmptfsum  25148  c1liplem1  25169  dvgt0lem2  25176  ftc1a  25210  ply1domn  25297  ply1divmo  25309  fta1b  25343  ig1peu  25345  coeeu  25395  plydivalg  25468  aaliou2b  25510  ulmss  25565  ulmcn  25567  efif1olem4  25710  efsubm  25716  logccv  25827  logbmpt  25947  logbfval  25949  cvxcl  26143  basellem4  26242  fsumdvdscom  26343  musum  26349  dvdsmulf1o  26352  fsumdvdsmul  26353  dchrelbasd  26396  dchrmulcl  26406  dchrinv  26418  lgsqrlem2  26504  lgsdchr  26512  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  2sqreulem4  26611  dchrisumlema  26645  dchrisumlem2  26647  chpdifbndlem2  26711  pntpbnd  26745  pntibndlem3  26749  axtgcont  26839  tgjustc1  26845  tgjustc2  26846  iscgrglt  26884  ercgrg  26887  idmot  26907  motco  26910  cnvmot  26911  motcgrg  26914  tgisline  26997  tghilberti2  27008  mirreu3  27024  mirmot  27045  ragperp  27087  foot  27092  mideu  27108  midf  27146  lmimot  27168  trgcopyeu  27176  f1otrgds  27239  f1otrg  27241  f1otrge  27242  xmstrkgc  27262  brbtwn2  27282  axlowdimlem15  27333  axcontlem2  27342  axcontlem10  27350  eengtrkg  27363  eengtrkge  27364  numedglnl  27523  usgredgreu  27594  uspgredg2vtxeu  27596  uspgredg2v  27600  usgredg2v  27603  wlkswwlksf1o  28253  wwlksnextinj  28273  clwlkclwwlkf1  28383  clwwlkf1  28422  frcond4  28643  frgrncvvdeqlem8  28679  frgrncvvdeq  28682  frgrwopreglem4  28688  numclwwlk1lem2f1  28730  grpoinvf  28903  nvmf  29016  vacn  29065  nmcvcn  29066  smcnlem  29068  sspg  29099  ssps  29101  sspmlem  29103  0lno  29161  blocni  29176  ipblnfi  29226  minvecolem7  29254  unopf1o  30287  cnvunop  30289  unoplin  30291  counop  30292  hmopadj2  30312  hmoplin  30313  bralnfn  30319  lnopeq0i  30378  hmops  30391  hmopm  30392  hmopco  30394  lnconi  30404  cnlnadjlem2  30439  adjmul  30463  adjadd  30464  cdjreui  30803  disjxpin  30936  off2  30987  2ndresdju  30995  fnpreimac  31017  suppovss  31026  f1od2  31065  xrofsup  31099  s3f1  31230  ccatf1  31232  swrdf1  31237  odutos  31255  dfmgc2lem  31282  dfmgc2  31283  pwrssmgc  31287  mgcf1o  31290  abliso  31314  symgcntz  31363  tocyccntz  31420  archiabllem1  31456  archiabllem2  31460  suborng  31523  xrge0slmod  31557  nsgmgc  31606  intlidl  31611  rhmpreimaidl  31612  idlinsubrg  31617  rhmimaidl  31618  prmidl2  31625  idlmulssprm  31626  isprmidlc  31632  rhmpreimaprmidl  31636  qsidomlem1  31637  qsidomlem2  31638  mxidlprm  31649  ssmxidllem  31650  lindsun  31715  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  1smat1  31763  submateq  31768  madjusmdetlem3  31788  zart0  31838  pstmxmet  31856  ofcf  32080  ldgenpisys  32143  rossros  32157  inelcarsg  32287  sibfof  32316  sitmf  32328  hgt750lemb  32645  erdszelem4  33165  erdszelem9  33170  erdsze2lem2  33175  cnpconn  33201  pconnconn  33202  txpconn  33203  ptpconn  33204  cvxpconn  33213  cvxsconn  33214  iccllysconn  33221  cvmseu  33247  cvmliftmo  33255  cvmlift2lem5  33278  cvmlift2lem9  33282  mrsubff1  33485  elmrsubrn  33491  mrsubco  33492  msubff1  33527  mvhf1  33530  ssltd  33995  oldbday  34090  segconeu  34322  fnessref  34555  neibastop1  34557  filnetlem3  34578  onsuct0  34639  unblimceq0lem  34695  unbdqndv2  34700  knoppndv  34723  irrdiff  35506  uncf  35765  fin2so  35773  lindsadd  35779  poimirlem4  35790  poimirlem13  35799  poimirlem14  35800  poimirlem26  35812  heicant  35821  mblfinlem2  35824  ftc1anc  35867  sdclem1  35910  isbnd3  35951  prdsbnd  35960  ismtycnv  35969  ismtyhmeolem  35971  ismtyres  35975  bfplem1  35989  bfplem2  35990  bfp  35991  rrnmet  35996  ismrer1  36005  iccbnd  36007  grpokerinj  36060  isdrngo2  36125  rngogrphom  36138  rngohomco  36141  rngoisocnv  36148  iscringd  36165  erprt  36894  lfl0f  37090  lkrlss  37116  lshpsmreu  37130  linepsubN  37773  pmapsub  37789  lautcnv  38111  lautco  38118  idltrn  38171  cdleme50f1  38564  cdleme50laut  38568  istendod  38783  dihf11  39288  dih1dimatlem  39350  lcfl7N  39522  lcfrlem9  39571  mapd1o  39669  hdmapf1oN  39886  hgmapf1oN  39924  qsalrel  40222  ismhmd  40245  fsuppind  40286  sn-negex12  40405  nacsfix  40541  rmxypairf1o  40740  wepwsolem  40874  dnnumch3  40879  fnwe2  40885  mpaaeu  40982  idomsubgmo  41030  mon1psubm  41038  deg1mhm  41039  isotone1  41665  isotone2  41666  mnringmulrcld  41853  disjxp1  42624  disjf1  42727  wessf1ornlem  42729  projf1o  42743  sumnnodd  43178  lptioo2  43179  lptioo1  43180  cncfshift  43422  cncfperiod  43427  dvnprodlem1  43494  fourierdlem42  43697  nnfoctbdjlem  44000  isomennd  44076  smflimlem6  44321  fsetsnf1  44557  cfsetsnfsetf1  44564  otiunsndisjX  44782  imasetpreimafvbijlemf1  44867  iccpartgt  44890  icceuelpart  44899  ichnreuop  44935  sprsymrelfolem2  44956  sprsymrelf  44958  prproropf1o  44970  reupr  44985  reuopreuprim  44989  isomuspgrlem2c  45293  isomuspgr  45297  ismgmd  45341  mgmhmpropd  45350  mgmhmf1o  45352  idmgmhm  45353  issubmgm2  45355  rabsubmgmd  45356  resmgmhm  45363  resmgmhm2  45364  resmgmhm2b  45365  mgmhmco  45366  submgmacs  45369  opmpoismgm  45372  mgmplusgiopALT  45399  isrnghm2d  45470  c0mgm  45478  c0mhm  45479  lidlmmgm  45494  2zlidl  45503  rnghmsscmap2  45542  rnghmsscmap  45543  rnghmsubcsetclem2  45545  rhmsscmap2  45588  rhmsscmap  45589  rhmsubcsetclem2  45591  rhmsscrnghm  45595  rhmsubcrngclem2  45597  srhmsubc  45645  fldhmsubc  45653  rhmsubc  45659  srhmsubcALTV  45663  fldhmsubcALTV  45671  rhmsubcALTV  45677  lindslinindsimp1  45809  1arymaptf1  45999  2arymaptf1  46010  toslat  46279  catprsc  46305  catprsc2  46306  isthincd  46329  isthincd2  46330  functhinclem4  46336  thincfth  46340  thincciso  46341