Theorem ralrimivva 3207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079

This theorem is used by:  disjord  5097  disjxiun  5105  otsndisj  5501  otiunsndisj  5502  swopo  5579  issod  5603  reuop  6294  fcof1  7285  fliftfund  7311  isof1oidb  7322  isof1oopb  7323  soisores  7325  soisoi  7326  isocnv  7328  f1oiso  7349  oveqrspc2v  7439  oprres  7580  caovclg  7604  caovcomg  7607  off  7694  coof  7700  caofidlcan  7714  caofrss  7715  caonncan  7720  dmmpog  8069  fnmpoovd  8080  fmpoco  8088  fsplitfpar  8111  poxp  8122  fvmpocurryd  8265  smo11  8349  smoiso2  8354  omsmo  8642  nnasmo  8647  coflton  8655  qsdisj2  8791  eroprf  8811  dom2lem  8987  omxpenlem  9064  xpf1o  9125  unxpdomlem3  9216  fofinf1o  9287  dffi3  9389  supmo  9410  infmo  9455  inf3lem6  9600  cantnf  9660  rankxplim  9849  fseqenlem1  10015  fodomacn  10047  iunfictbso  10105  cofsmo  10259  infpssrlem5  10297  enfin2i  10311  fin23lem23  10316  fin23lem27  10318  fin23lem28  10330  compssiso  10364  ltordlem  11745  cju  12220  axdc4uzlem  14026  seqcaopr2  14081  seqhomo  14092  wrd2ind  14767  cshf1  14854  s3sndisj  15011  s3iunsndisj  15012  climcn2  15651  addcn2  15652  mulcn2  15654  o1of2  15671  isercolllem1  15723  fsum2dlem  15828  fsumcom2  15832  fprodser  16010  fprod2dlem  16041  fprodcom2  16045  isprm6  16779  crth  16843  eulerthlem2  16847  vdwlem12  17058  cshwsdisj  17164  imasaddfnlem  17588  imasvscafn  17597  mreexexd  17710  iscatd  17735  oppccomfpropd  17789  isofn  17838  sectmon  17845  ssctr  17888  ssceq  17889  catsubcat  17902  issubc3  17912  fullsubc  17913  fullresc  17914  isfuncd  17928  idfucl  17944  cofucl  17951  funcres2b  17960  fulloppc  17987  fthoppc  17988  idffth  17998  cofull  17999  cofth  18000  ressffth  18003  setcmon  18150  setcepi  18151  resssetc  18155  resscatc  18172  catciso  18174  fthestrcsetc  18212  fullestrcsetc  18213  embedsetcestrclem  18219  fthsetcestrc  18227  fullsetcestrc  18228  evlfcl  18284  uncfcurf  18301  hofcl  18321  yonedalem3  18342  yonedainv  18343  yonffthlem  18344  yoniso  18347  isdrs2  18368  isposd  18384  pospropd  18387  poslubmo  18471  posglbmo  18472  chnpof1  18692  mgmplusf  18714  ismgmd  18716  issstrmgm  18717  opifismgm  18723  mgmhmpropd  18762  mgmhmf1o  18764  idmgmhm  18765  issubmgm2  18767  rabsubmgmd  18768  resmgmhm  18775  resmgmhm2  18776  resmgmhm2b  18777  mgmhmco  18778  submgmacs  18781  issgrpd  18794  sgrppropd  18795  ismndd  18820  mndpropd  18823  issubmnd  18825  mndinvmod  18828  ismhmd  18850  mhmpropd  18856  idmhm  18859  mhmf1o  18860  issubmd  18870  mndissubm  18871  0mhm  18884  resmhm  18885  resmhm2  18886  resmhm2b  18887  mhmco  18888  submacs  18892  prdspjmhm  18894  pwsdiagmhm  18896  pwsco1mhm  18897  pwsco2mhm  18898  gsumwspan  18911  frmdsssubm  18926  frmdup1  18929  grpsubf  19091  dfgrp3  19111  mhmmnd  19136  mhmfmhm  19137  issubg4  19218  grpissubg  19219  isnsg3  19232  nsgacs  19234  0nsg  19241  nsgid  19242  qus0subgadd  19276  cycsubmcom  19281  isghmd  19301  ghmmhm  19302  idghm  19307  ghmnsgima  19316  ghmnsgpreima  19317  ghmf1  19322  kerf1ghm  19323  ghmf1o  19324  gaid  19375  subgga  19376  gass  19377  gasubg  19378  cntzsgrpcl  19410  cntzsubm  19414  cntrsubgnsg  19419  lactghmga  19481  symgfixf1  19513  odf1  19638  sylow1lem2  19675  sylow2blem2  19697  sylow3lem1  19703  lsmssv  19719  smndlsmidm  19732  pj1eu  19772  efglem  19792  efgtf  19798  efgred  19824  efgredeu  19828  frgpmhm  19841  frgpuptf  19846  frgpuplem  19848  mulgmhm  19903  ghmcmn  19907  invghm  19909  ablnsg  19923  imasabl  19952  cygabl  19967  gsum2d2lem  20049  gsum2d2  20050  gsumcom2  20051  dprd2d2  20122  ablfaclem2  20164  srgfcl  20284  srgcom4lem  20301  srglmhm  20309  srgrmhm  20310  ringcomlem  20369  isrnghm2d  20539  c0mgm  20548  c0mhm  20549  isrhm2d  20580  subrngringnsg  20663  issubrng2  20668  subrngint  20670  issubrg2  20702  subrgint  20705  rnghmsscmap2  20739  rnghmsscmap  20740  rnghmsubcsetclem2  20742  rhmsscmap2  20768  rhmsscmap  20769  rhmsubcsetclem2  20771  rhmsscrnghm  20775  rhmsubcrngclem2  20777  srhmsubc  20790  rhmsubc  20799  fldhmsubc  20899  primefld  20919  abvn0b  20950  suborng  20990  islmodd  20998  lmodscaf  21016  lmodprop2d  21056  islssd  21067  islss4  21094  lssacs  21099  lsspropd  21149  islmhmd  21171  lmhmima  21179  lmhmpreima  21180  reslmhm  21184  lspextmo  21188  lsmcl  21215  pj1lmhm  21232  islbs2  21289  issubrgd  21321  dflidl2rng  21354  rnglidlmmgm  21390  rhmpreimaidl  21427  rngqiprnglin  21453  prmidl2  21477  idlmulssprm  21478  isprmidlc  21483  rhmpreimaprmidl  21490  qsidomlem1  21491  qsidomlem2  21492  ssdifidllem  21495  ssdifidlprm  21497  prmidlsubm  21498  expmhm  21597  nn0srg  21598  prmirredlem  21633  expghm  21636  mulgghm2  21637  domnchr  21693  znf1o  21712  zntoslem  21717  znfld  21721  cygznlem3  21730  phlipf  21813  dsmmlss  21905  uvcf1  21953  frlmlbs  21958  lindff1  21981  lindfrn  21982  f1lindf  21983  issubassa2  22053  mvrf1  22146  mplsubglem  22159  mplsubrg  22165  mplcoe5lem  22201  mplcoe2  22203  mplind  22232  evlslem2  22241  evlseu  22245  mhplss  22329  ply1sclf1  22461  evls1maplmhm  22548  mamucl  22569  mamuass  22570  mamudi  22571  mamudir  22572  mamuvs1  22573  mamuvs2  22574  matbas2d  22591  mamumat1cl  22607  mamulid  22609  mamurid  22610  mat1mhm  22652  dmatid  22663  dmatsubcl  22666  dmatsgrp  22667  dmatmulcl  22668  dmatsrng  22669  dmatcrng  22670  scmatscmiddistr  22676  scmatscm  22681  scmatsgrp  22687  scmatsrng  22688  scmatcrng  22689  scmatsgrp1  22690  scmatsrng1  22691  scmatf1  22699  scmatmhm  22702  mavmul0g  22721  mdet1  22769  mdetunilem9  22788  mdetuni0  22789  mdetmul  22791  madutpos  22810  smadiadetlem4  22837  1elcpmat  22883  cpmatacl  22884  cpmatmcl  22887  mat2pmatf1  22897  mat2pmatmul  22899  mat2pmat1  22900  mat2pmatlin  22903  m2cpm  22909  m2cpminvid  22921  m2cpminvid2  22923  decpmatmul  22940  pmatcollpw1  22944  monmatcollpw  22947  pmatcollpw  22949  pmatcollpw3lem  22951  pmatcollpwscmatlem2  22958  pm2mpf1  22967  mp2pm2mplem4  22977  pm2mpmhmlem2  22987  chp0mat  23014  chpidmat  23015  tgclb  23138  mretopd  23260  toponmre  23261  iscldtop  23263  ordtbaslem  23356  ordtbas2  23359  cnt0  23514  haust1  23520  cnhaus  23522  isreg2  23545  dishaus  23550  ordthaus  23552  dfconn2  23587  iunconn  23596  clsconn  23598  2ndcomap  23626  dis2ndc  23628  llynlly  23645  restnlly  23650  restlly  23651  islly2  23652  llyidm  23656  nllyidm  23657  hausllycmp  23662  kgentopon  23706  txbas  23735  ptbasin2  23746  ptbasfi  23749  txcnp  23788  txcnmpt  23792  pthaus  23806  tx1stc  23818  xkococnlem  23827  xkococn  23828  cnmpt21  23839  qtoptop2  23867  qtopeu  23884  kqt0lem  23904  isr0  23905  regr1lem2  23908  kqreglem1  23909  kqreglem2  23910  kqnrmlem1  23911  kqnrmlem2  23912  nrmr0reg  23917  reghmph  23961  nrmhmph  23962  txswaphmeo  23973  qtophmeo  23985  fbun  24008  trfbas2  24011  isfil2  24024  infil  24031  trfil2  24055  filssufilg  24079  hausflim  24149  fclsnei  24187  fclsfnflim  24195  flimfnfcls  24196  ptcmplem1  24220  clssubg  24277  tgpconncomp  24281  qustgplem  24289  tsmsfbas  24296  utoptop  24402  iducn  24450  cstucnd  24451  isxmetd  24494  isxmet2d  24495  xmettpos  24517  prdsdsf  24535  prdsmet  24538  ressprdsds  24539  imasdsf1olem  24541  imasf1oxmet  24543  imasf1omet  24544  blfvalps  24551  xmetresbl  24605  metss2  24680  comet  24681  stdbdmet  24684  stdbdmopn  24686  methaus  24688  met2ndci  24690  metustfbas  24725  nrmmetd  24742  subgngp  24803  ngptgp  24804  sranlm  24852  nlmvscnlem1  24854  nlmvscn  24855  nrginvrcn  24860  lssnlm  24869  nghmcn  24913  qtopbaslem  24926  reconn  24997  xmetdcn2  25006  metdscn  25025  metnrm  25031  elcncf1di  25065  cncfcdm  25068  mulc1cncf  25075  cncfco  25077  reparphti  25167  isncvsngpd  25320  tcphcph  25407  ipcnlem1  25415  ipcn  25416  iscfil3  25443  bcthlem5  25498  rrxmet  25578  minveclem3  25599  minveclem7  25605  ovolicc2lem4  25690  dyadmbl  25770  volcn  25776  itg1addlem1  25862  itg1addlem2  25867  itg1addlem4  25869  mbfi1fseqlem1  25885  mbfi1fseqlem3  25887  mbfi1fseqlem4  25888  mbfi1fseqlem5  25889  dvmptfsum  26145  c1liplem1  26166  dvgt0lem2  26173  ftc1a  26207  ply1domn  26292  ply1divmo  26304  fta1b  26340  ig1peu  26343  coeeu  26393  plydivalg  26471  aaliou2b  26515  ulmss  26571  ulmcn  26573  efif1olem4  26721  efsubm  26727  logccv  26839  logbmpt  26964  logbfval  26966  cvxcl  27160  basellem4  27259  fsumdvdscom  27360  musum  27366  mpodvdsmulf1o  27369  fsumdvdsmul  27370  dvdsmulf1o  27371  dchrelbasd  27414  dchrmulcl  27424  dchrinv  27436  lgsqrlem2  27522  lgsdchr  27530  lgseisenlem2  27551  lgsquadlem1  27555  lgsquadlem2  27556  2sqreulem4  27629  dchrisumlema  27663  dchrisumlem2  27665  chpdifbndlem2  27729  pntpbnd  27763  pntibndlem3  27767  sltsd  27972  oldbday  28105  addsprop  28180  mulcutlem  28335  divsmo  28388  om2noseqf1o  28505  om2noseqiso  28506  axtgcont  28749  tgjustc1  28755  tgjustc2  28756  iscgrglt  28794  ercgrg  28797  idmot  28817  motco  28820  cnvmot  28821  motcgrg  28824  tgisline  28911  tghilberti2  28922  mirreu3  28942  mirmot  28963  ragperp  29008  foot  29013  mideu  29030  midf  29096  lmimot  29118  trgcopyeu  29128  prlngmolem1  29213  f1otrgds  29229  f1otrg  29231  f1otrge  29232  xmstrkgc  29246  brbtwn2  29266  axlowdimlem15  29317  axcontlem2  29326  axcontlem10  29334  eengtrkg  29347  eengtrkge  29348  numedglnl  29505  usgredgreu  29579  uspgredg2vtxeu  29581  uspgredg2v  29585  usgredg2v  29588  wlkswwlksf1o  30239  wwlksnextinj  30259  clwlkclwwlkf1  30372  clwwlkf1  30411  frcond4  30632  frgrncvvdeqlem8  30668  frgrncvvdeq  30671  frgrwopreglem4  30677  numclwwlk1lem2f1  30719  nrt2irr  30835  grpoinvf  30895  nvmf  31008  vacn  31057  nmcvcn  31058  smcnlem  31060  sspg  31091  ssps  31093  sspmlem  31095  0lno  31153  blocni  31168  ipblnfi  31218  minvecolem7  31246  unopf1o  32279  cnvunop  32281  unoplin  32283  counop  32284  hmopadj2  32304  hmoplin  32305  bralnfn  32311  lnopeq0i  32370  hmops  32383  hmopm  32384  hmopco  32386  lnconi  32396  cnlnadjlem2  32431  adjmul  32455  adjadd  32456  cdjreui  32795  disjxpin  32944  off2  32997  2ndresdju  33005  fnpreimac  33026  suppovss  33037  f1od2  33075  xrofsup  33123  s3f1  33276  ccatf1  33278  swrdf1  33285  odutos  33297  dfmgc2lem  33324  dfmgc2  33325  pwrssmgc  33329  mgcf1o  33332  mndlactf1  33355  mndractf1  33357  abliso  33364  symgcntz  33414  tocyccntz  33473  conjga  33499  fxpsubrg  33503  archiabllem1  33522  archiabllem2  33526  urpropd  33559  elrgspnlem2  33572  rlocf1  33603  rrgsubm  33613  subrdom  33614  ricdomn1  33618  xrge0slmod  33677  nsgmgc  33730  intlidl  33737  idlinsubrg  33748  rhmimaidl  33749  mxidlprm  33762  mxidlirredi  33763  ssmxidllem  33765  drnglring  33791  dflringlem2  33794  rsprprmprmidl  33821  rsprprmprmidlb  33822  rprmirred  33830  rprmirredb  33831  1arithufdlem4  33846  selvply1rhmlema  33917  selvply1rhmlem1  33919  mplidomlem  33926  extvfvcl  33935  mplvrpmga  33944  ply1degltdimlem  34021  ply1degltdim  34022  lindsun  34024  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  lactlmhm  34033  assalactf1o  34034  minplyirred  34110  constrsdrg  34174  1smat1  34203  submateq  34208  madjusmdetlem3  34228  zart0  34278  pstmxmet  34296  ofcf  34502  ldgenpisys  34565  rossros  34579  inelcarsg  34710  sibfof  34739  sitmf  34751  hgt750lemb  35052  erdszelem4  35694  erdszelem9  35699  erdsze2lem2  35704  cnpconn  35730  pconnconn  35731  txpconn  35732  ptpconn  35733  cvxpconn  35742  cvxsconn  35743  iccllysconn  35750  cvmseu  35776  cvmliftmo  35784  cvmlift2lem5  35807  cvmlift2lem9  35811  mrsubff1  36014  elmrsubrn  36020  mrsubco  36021  msubff1  36056  mvhf1  36059  r1peuqusdeg1  36143  segconeu  36511  nmulprop  36690  nadddilem4  36723  fnessref  36896  neibastop1  36898  filnetlem3  36919  onsuct0  36980  weiunlem  37002  mh-inf3f1  37080  unblimceq0lem  37123  unbdqndv2  37128  knoppndv  37151  irrdiff  37998  uncf  38278  fin2so  38286  lindsadd  38292  poimirlem4  38303  poimirlem13  38312  poimirlem14  38313  poimirlem26  38325  heicant  38334  mblfinlem2  38337  ftc1anc  38380  sdclem1  38422  isbnd3  38463  prdsbnd  38472  ismtycnv  38481  ismtyhmeolem  38483  ismtyres  38487  bfplem1  38501  bfplem2  38502  bfp  38503  rrnmet  38508  ismrer1  38517  iccbnd  38519  grpokerinj  38572  isdrngo2  38637  rngogrphom  38650  rngohomco  38653  rngoisocnv  38660  iscringd  38677  eqvreldisj1  39604  erprt  39675  lfl0f  39871  lkrlss  39897  lshpsmreu  39911  linepsubN  40554  pmapsub  40570  lautcnv  40892  lautco  40899  idltrn  40952  cdleme50f1  41345  cdleme50laut  41349  istendod  41564  dihf11  42069  dih1dimatlem  42131  lcfl7N  42303  lcfrlem9  42352  mapd1o  42450  hdmapf1oN  42667  hgmapf1oN  42705  fmpocos  43032  qsalrel  43037  rediveud  43232  imacrhmcl  43316  evlselv  43349  fsuppind  43350  nacsfix  43471  rmxypairf1o  43666  wepwsolem  43797  dnnumch3  43802  fnwe2  43808  mpaaeu  43905  idomsubgmo  43948  mon1psubm  43954  deg1mhm  43955  isotone1  44802  isotone2  44803  mnringmulrcld  44980  traxext  45714  disjxp1  45817  disjf1  45929  wessf1ornlem  45931  projf1o  45942  sumnnodd  46374  lptioo2  46375  lptioo1  46376  cncfshift  46616  cncfperiod  46621  dvnprodlem1  46688  fourierdlem42  46891  nnfoctbdjlem  47197  isomennd  47273  smflimlem6  47518  fsetsnf1  47817  cfsetsnfsetf1  47824  otiunsndisjX  48044  imasetpreimafvbijlemf1  48181  iccpartgt  48204  icceuelpart  48213  ichnreuop  48249  sprsymrelfolem2  48270  sprsymrelf  48272  prproropf1o  48284  reupr  48299  reuopreuprim  48303  uhgrimprop  48685  isuspgrim0lem  48686  upgrimtrls  48699  gpgprismgr4cycllem11  48898  opmpoismgm  48960  mgmplusgiopALT  48987  2zlidl  49033  rhmsubcALTV  49078  srhmsubcALTV  49118  fldhmsubcALTV  49126  lindslinindsimp1  49265  1arymaptf1  49450  2arymaptf1  49461  eqfnovd  49672  fmpodg  49675  toslat  49788  catprsc  49819  catprsc2  49820  oppcendc  49824  invfn  49836  iinfssclem2  49861  iinfssc  49863  iinfsubc  49864  discsubc  49870  nelsubclem  49873  resccatlem  49879  funchomf  49903  imasubclem2  49911  imaidfu  49916  imasubc  49957  imassc  49959  imasubc3  49962  fthcomf  49963  idfth  49964  cofidfth  49968  upeu2  49978  isnatd  50029  swapfffth  50089  diag1f1  50113  diag2f1  50115  fucoppc  50216  isthincd  50242  isthincd2  50243  oppcthinco  50245  oppcthinendcALT  50247  functhinclem4  50253  functhincfun  50255  thincfth  50258  thincciso  50259  thinccisod  50260  functermc  50314  arweuthinc  50335  arweutermc  50336  diagffth  50344  funcsn  50347  0fucterm  50349