Theorem ralrimivva 3180

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

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 3053

This theorem is referenced by:  disjord  5088  disjxiun  5096  otsndisj  5468  otiunsndisj  5469  swopo  5544  issod  5568  reuop  6252  fcof1  7236  fliftfund  7262  isof1oidb  7273  isof1oopb  7274  soisores  7276  soisoi  7277  isocnv  7279  f1oiso  7300  oveqrspc2v  7388  oprres  7529  caovclg  7553  caovcomg  7556  off  7643  coof  7649  caofidlcan  7663  caofrss  7664  caonncan  7669  dmmpog  8021  fnmpoovd  8032  fmpoco  8040  fsplitfpar  8063  poxp  8073  fvmpocurryd  8216  smo11  8299  smoiso2  8304  omsmo  8589  nnasmo  8594  coflton  8602  qsdisj2  8737  eroprf  8757  dom2lem  8934  omxpenlem  9011  xpf1o  9072  unxpdomlem3  9163  fofinf1o  9237  dffi3  9339  supmo  9360  infmo  9405  inf3lem6  9547  cantnf  9607  rankxplim  9796  fseqenlem1  9939  fodomacn  9971  iunfictbso  10029  cofsmo  10184  infpssrlem5  10222  enfin2i  10236  fin23lem23  10241  fin23lem27  10243  fin23lem28  10255  compssiso  10289  ltordlem  11667  cju  12146  axdc4uzlem  13911  seqcaopr2  13966  seqhomo  13977  wrd2ind  14651  cshf1  14738  s3sndisj  14895  s3iunsndisj  14896  climcn2  15521  addcn2  15522  mulcn2  15524  o1of2  15541  isercolllem1  15593  fsum2dlem  15698  fsumcom2  15702  fprodser  15877  fprod2dlem  15908  fprodcom2  15912  isprm6  16646  crth  16710  eulerthlem2  16714  vdwlem12  16925  cshwsdisj  17031  imasaddfnlem  17454  imasvscafn  17463  mreexexd  17576  iscatd  17601  oppccomfpropd  17655  isofn  17704  sectmon  17711  ssctr  17754  ssceq  17755  catsubcat  17768  issubc3  17778  fullsubc  17779  fullresc  17780  isfuncd  17794  idfucl  17810  cofucl  17817  funcres2b  17826  fulloppc  17853  fthoppc  17854  idffth  17864  cofull  17865  cofth  17866  ressffth  17869  setcmon  18016  setcepi  18017  resssetc  18021  resscatc  18038  catciso  18040  fthestrcsetc  18078  fullestrcsetc  18079  embedsetcestrclem  18085  fthsetcestrc  18093  fullsetcestrc  18094  evlfcl  18150  uncfcurf  18167  hofcl  18187  yonedalem3  18208  yonedainv  18209  yonffthlem  18210  yoniso  18213  isdrs2  18234  isposd  18250  pospropd  18253  poslubmo  18337  posglbmo  18338  chnpof1  18558  mgmplusf  18580  ismgmd  18582  issstrmgm  18583  opifismgm  18589  mgmhmpropd  18628  mgmhmf1o  18630  idmgmhm  18631  issubmgm2  18633  rabsubmgmd  18634  resmgmhm  18641  resmgmhm2  18642  resmgmhm2b  18643  mgmhmco  18644  submgmacs  18647  issgrpd  18660  sgrppropd  18661  ismndd  18686  mndpropd  18689  issubmnd  18691  mndinvmod  18694  ismhmd  18716  mhmpropd  18722  idmhm  18725  mhmf1o  18726  issubmd  18736  mndissubm  18737  0mhm  18749  resmhm  18750  resmhm2  18751  resmhm2b  18752  mhmco  18753  submacs  18757  prdspjmhm  18759  pwsdiagmhm  18761  pwsco1mhm  18762  pwsco2mhm  18763  gsumwspan  18776  frmdsssubm  18791  frmdup1  18794  grpsubf  18954  dfgrp3  18974  mhmmnd  18999  mhmfmhm  19000  issubg4  19080  grpissubg  19081  isnsg3  19094  nsgacs  19096  0nsg  19103  nsgid  19104  qus0subgadd  19133  cycsubmcom  19138  isghmd  19159  ghmmhm  19160  idghm  19165  ghmnsgima  19174  ghmnsgpreima  19175  ghmf1  19180  kerf1ghm  19181  ghmf1o  19182  gaid  19233  subgga  19234  gass  19235  gasubg  19236  cntzsgrpcl  19268  cntzsubm  19272  cntrsubgnsg  19277  lactghmga  19339  symgfixf1  19371  odf1  19496  sylow1lem2  19533  sylow2blem2  19555  sylow3lem1  19561  lsmssv  19577  smndlsmidm  19590  pj1eu  19630  efglem  19650  efgtf  19656  efgred  19682  efgredeu  19686  frgpmhm  19699  frgpuptf  19704  frgpuplem  19706  mulgmhm  19761  ghmcmn  19765  invghm  19767  ablnsg  19781  imasabl  19810  cygabl  19825  gsum2d2lem  19907  gsum2d2  19908  gsumcom2  19909  dprd2d2  19980  ablfaclem2  20022  srgfcl  20136  srgcom4lem  20153  srglmhm  20161  srgrmhm  20162  ringcomlem  20219  isrnghm2d  20391  c0mgm  20400  c0mhm  20401  isrhm2d  20427  subrngringnsg  20491  issubrng2  20496  subrngint  20498  issubrg2  20530  subrgint  20533  rnghmsscmap2  20567  rnghmsscmap  20568  rnghmsubcsetclem2  20570  rhmsscmap2  20596  rhmsscmap  20597  rhmsubcsetclem2  20599  rhmsscrnghm  20603  rhmsubcrngclem2  20605  srhmsubc  20618  rhmsubc  20627  fldhmsubc  20723  primefld  20743  abvn0b  20774  suborng  20814  islmodd  20822  lmodscaf  20840  lmodprop2d  20880  islssd  20891  islss4  20918  lssacs  20923  lsspropd  20974  islmhmd  20996  lmhmima  21004  lmhmpreima  21005  reslmhm  21009  lspextmo  21013  lsmcl  21040  pj1lmhm  21057  islbs2  21114  issubrgd  21146  dflidl2rng  21178  rnglidlmmgm  21205  rhmpreimaidl  21237  rngqiprnglin  21262  expmhm  21396  nn0srg  21397  prmirredlem  21432  expghm  21435  mulgghm2  21436  domnchr  21492  znf1o  21511  zntoslem  21516  znfld  21520  cygznlem3  21529  phlipf  21612  dsmmlss  21704  uvcf1  21752  frlmlbs  21757  lindff1  21780  lindfrn  21781  f1lindf  21782  issubassa2  21853  mvrf1  21946  mplsubglem  21959  mplsubrg  21965  mplcoe5lem  21999  mplcoe2  22001  mplind  22030  evlslem2  22039  evlseu  22043  mhplss  22103  ply1sclf1  22236  evls1maplmhm  22326  mamucl  22350  mamuass  22351  mamudi  22352  mamudir  22353  mamuvs1  22354  mamuvs2  22355  matbas2d  22372  mamumat1cl  22388  mamulid  22390  mamurid  22391  mat1mhm  22433  dmatid  22444  dmatsubcl  22447  dmatsgrp  22448  dmatmulcl  22449  dmatsrng  22450  dmatcrng  22451  scmatscmiddistr  22457  scmatscm  22462  scmatsgrp  22468  scmatsrng  22469  scmatcrng  22470  scmatsgrp1  22471  scmatsrng1  22472  scmatf1  22480  scmatmhm  22483  mavmul0g  22502  mdet1  22550  mdetunilem9  22569  mdetuni0  22570  mdetmul  22572  madutpos  22591  smadiadetlem4  22618  1elcpmat  22664  cpmatacl  22665  cpmatmcl  22668  mat2pmatf1  22678  mat2pmatmul  22680  mat2pmat1  22681  mat2pmatlin  22684  m2cpm  22690  m2cpminvid  22702  m2cpminvid2  22704  decpmatmul  22721  pmatcollpw1  22725  monmatcollpw  22728  pmatcollpw  22730  pmatcollpw3lem  22732  pmatcollpwscmatlem2  22739  pm2mpf1  22748  mp2pm2mplem4  22758  pm2mpmhmlem2  22768  chp0mat  22795  chpidmat  22796  tgclb  22919  mretopd  23041  toponmre  23042  iscldtop  23044  ordtbaslem  23137  ordtbas2  23140  cnt0  23295  haust1  23301  cnhaus  23303  isreg2  23326  dishaus  23331  ordthaus  23333  dfconn2  23368  iunconn  23377  clsconn  23379  2ndcomap  23407  dis2ndc  23409  llynlly  23426  restnlly  23431  restlly  23432  islly2  23433  llyidm  23437  nllyidm  23438  hausllycmp  23443  kgentopon  23487  txbas  23516  ptbasin2  23527  ptbasfi  23530  txcnp  23569  txcnmpt  23573  pthaus  23587  tx1stc  23599  xkococnlem  23608  xkococn  23609  cnmpt21  23620  qtoptop2  23648  qtopeu  23665  kqt0lem  23685  isr0  23686  regr1lem2  23689  kqreglem1  23690  kqreglem2  23691  kqnrmlem1  23692  kqnrmlem2  23693  nrmr0reg  23698  reghmph  23742  nrmhmph  23743  txswaphmeo  23754  qtophmeo  23766  fbun  23789  trfbas2  23792  isfil2  23805  infil  23812  trfil2  23836  filssufilg  23860  hausflim  23930  fclsnei  23968  fclsfnflim  23976  flimfnfcls  23977  ptcmplem1  24001  clssubg  24058  tgpconncomp  24062  qustgplem  24070  tsmsfbas  24077  utoptop  24183  iducn  24231  cstucnd  24232  isxmetd  24275  isxmet2d  24276  xmettpos  24298  prdsdsf  24316  prdsmet  24319  ressprdsds  24320  imasdsf1olem  24322  imasf1oxmet  24324  imasf1omet  24325  blfvalps  24332  xmetresbl  24386  metss2  24461  comet  24462  stdbdmet  24465  stdbdmopn  24467  methaus  24469  met2ndci  24471  metustfbas  24506  nrmmetd  24523  subgngp  24584  ngptgp  24585  sranlm  24633  nlmvscnlem1  24635  nlmvscn  24636  nrginvrcn  24641  lssnlm  24650  nghmcn  24694  qtopbaslem  24707  reconn  24778  xmetdcn2  24787  metdscn  24806  metnrm  24812  elcncf1di  24849  cncfcdm  24852  mulc1cncf  24859  cncfco  24861  reparphti  24957  reparphtiOLD  24958  isncvsngpd  25111  tcphcph  25198  ipcnlem1  25206  ipcn  25207  iscfil3  25234  bcthlem5  25289  rrxmet  25369  minveclem3  25390  minveclem7  25396  ovolicc2lem4  25482  dyadmbl  25562  volcn  25568  itg1addlem1  25654  itg1addlem2  25659  itg1addlem4  25661  mbfi1fseqlem1  25677  mbfi1fseqlem3  25679  mbfi1fseqlem4  25680  mbfi1fseqlem5  25681  dvmptfsum  25940  c1liplem1  25962  dvgt0lem2  25969  ftc1a  26005  ply1domn  26090  ply1divmo  26102  fta1b  26138  ig1peu  26141  coeeu  26191  plydivalg  26268  aaliou2b  26310  ulmss  26367  ulmcn  26369  efif1olem4  26515  efsubm  26521  logccv  26633  logbmpt  26759  logbfval  26761  cvxcl  26956  basellem4  27055  fsumdvdscom  27156  musum  27162  mpodvdsmulf1o  27165  fsumdvdsmul  27166  dvdsmulf1o  27167  fsumdvdsmulOLD  27168  dchrelbasd  27211  dchrmulcl  27221  dchrinv  27233  lgsqrlem2  27319  lgsdchr  27327  lgseisenlem2  27348  lgsquadlem1  27352  lgsquadlem2  27353  2sqreulem4  27426  dchrisumlema  27460  dchrisumlem2  27462  chpdifbndlem2  27526  pntpbnd  27560  pntibndlem3  27564  sltsd  27769  oldbday  27902  addsprop  27977  mulcutlem  28132  divsmo  28185  om2noseqf1o  28302  om2noseqiso  28303  axtgcont  28546  tgjustc1  28552  tgjustc2  28553  iscgrglt  28591  ercgrg  28594  idmot  28614  motco  28617  cnvmot  28618  motcgrg  28621  tgisline  28704  tghilberti2  28715  mirreu3  28731  mirmot  28752  ragperp  28794  foot  28799  mideu  28815  midf  28853  lmimot  28875  trgcopyeu  28883  f1otrgds  28946  f1otrg  28948  f1otrge  28949  xmstrkgc  28963  brbtwn2  28983  axlowdimlem15  29034  axcontlem2  29043  axcontlem10  29051  eengtrkg  29064  eengtrkge  29065  numedglnl  29222  usgredgreu  29296  uspgredg2vtxeu  29298  uspgredg2v  29302  usgredg2v  29305  wlkswwlksf1o  29957  wwlksnextinj  29977  clwlkclwwlkf1  30090  clwwlkf1  30129  frcond4  30350  frgrncvvdeqlem8  30386  frgrncvvdeq  30389  frgrwopreglem4  30395  numclwwlk1lem2f1  30437  nrt2irr  30553  grpoinvf  30612  nvmf  30725  vacn  30774  nmcvcn  30775  smcnlem  30777  sspg  30808  ssps  30810  sspmlem  30812  0lno  30870  blocni  30885  ipblnfi  30935  minvecolem7  30963  unopf1o  31996  cnvunop  31998  unoplin  32000  counop  32001  hmopadj2  32021  hmoplin  32022  bralnfn  32028  lnopeq0i  32087  hmops  32100  hmopm  32101  hmopco  32103  lnconi  32113  cnlnadjlem2  32148  adjmul  32172  adjadd  32173  cdjreui  32512  disjxpin  32667  off2  32723  2ndresdju  32731  fnpreimac  32752  suppovss  32763  f1od2  32801  xrofsup  32850  s3f1  33032  ccatf1  33034  swrdf1  33041  odutos  33053  dfmgc2lem  33080  dfmgc2  33081  pwrssmgc  33085  mgcf1o  33088  mndlactf1  33111  mndractf1  33113  abliso  33121  symgcntz  33171  tocyccntz  33230  conjga  33256  fxpsubrg  33260  archiabllem1  33279  archiabllem2  33283  urpropd  33317  elrgspnlem2  33329  rlocf1  33359  rrgsubm  33370  subrdom  33371  xrge0slmod  33433  nsgmgc  33497  intlidl  33505  idlinsubrg  33516  rhmimaidl  33517  prmidl2  33526  idlmulssprm  33527  isprmidlc  33532  rhmpreimaprmidl  33536  qsidomlem1  33537  qsidomlem2  33538  ssdifidllem  33541  ssdifidlprm  33543  mxidlprm  33555  mxidlirredi  33556  ssmxidllem  33558  rsprprmprmidl  33607  rsprprmprmidlb  33608  rprmirred  33616  rprmirredb  33617  1arithufdlem4  33632  extvfvcl  33705  mplvrpmga  33714  ply1degltdimlem  33792  ply1degltdim  33793  lindsun  33795  fedgmullem1  33799  fedgmullem2  33800  fedgmul  33801  lactlmhm  33804  assalactf1o  33805  minplyirred  33881  constrsdrg  33945  1smat1  33974  submateq  33979  madjusmdetlem3  33999  zart0  34049  pstmxmet  34067  ofcf  34273  ldgenpisys  34336  rossros  34350  inelcarsg  34481  sibfof  34510  sitmf  34522  hgt750lemb  34826  erdszelem4  35401  erdszelem9  35406  erdsze2lem2  35411  cnpconn  35437  pconnconn  35438  txpconn  35439  ptpconn  35440  cvxpconn  35449  cvxsconn  35450  iccllysconn  35457  cvmseu  35483  cvmliftmo  35491  cvmlift2lem5  35514  cvmlift2lem9  35518  mrsubff1  35721  elmrsubrn  35727  mrsubco  35728  msubff1  35763  mvhf1  35766  r1peuqusdeg1  35850  segconeu  36218  fnessref  36564  neibastop1  36566  filnetlem3  36587  onsuct0  36648  weiunlem  36670  unblimceq0lem  36719  unbdqndv2  36724  knoppndv  36747  irrdiff  37544  uncf  37813  fin2so  37821  lindsadd  37827  poimirlem4  37838  poimirlem13  37847  poimirlem14  37848  poimirlem26  37860  heicant  37869  mblfinlem2  37872  ftc1anc  37915  sdclem1  37957  isbnd3  37998  prdsbnd  38007  ismtycnv  38016  ismtyhmeolem  38018  ismtyres  38022  bfplem1  38036  bfplem2  38037  bfp  38038  rrnmet  38043  ismrer1  38052  iccbnd  38054  grpokerinj  38107  isdrngo2  38172  rngogrphom  38185  rngohomco  38188  rngoisocnv  38195  iscringd  38212  eqvreldisj1  39141  erprt  39212  lfl0f  39408  lkrlss  39434  lshpsmreu  39448  linepsubN  40091  pmapsub  40107  lautcnv  40429  lautco  40436  idltrn  40489  cdleme50f1  40882  cdleme50laut  40886  istendod  41101  dihf11  41606  dih1dimatlem  41668  lcfl7N  41840  lcfrlem9  41889  mapd1o  41987  hdmapf1oN  42204  hgmapf1oN  42242  fmpocos  42569  qsalrel  42574  rediveud  42776  imacrhmcl  42847  evlselv  42908  fsuppind  42911  nacsfix  43032  rmxypairf1o  43231  wepwsolem  43362  dnnumch3  43367  fnwe2  43373  mpaaeu  43470  idomsubgmo  43513  mon1psubm  43519  deg1mhm  43520  isotone1  44367  isotone2  44368  mnringmulrcld  44547  traxext  45296  disjxp1  45392  disjf1  45505  wessf1ornlem  45507  projf1o  45518  sumnnodd  45953  lptioo2  45954  lptioo1  45955  cncfshift  46195  cncfperiod  46200  dvnprodlem1  46267  fourierdlem42  46470  nnfoctbdjlem  46776  isomennd  46852  smflimlem6  47097  fsetsnf1  47375  cfsetsnfsetf1  47382  otiunsndisjX  47602  imasetpreimafvbijlemf1  47727  iccpartgt  47750  icceuelpart  47759  ichnreuop  47795  sprsymrelfolem2  47816  sprsymrelf  47818  prproropf1o  47830  reupr  47845  reuopreuprim  47849  uhgrimprop  48215  isuspgrim0lem  48216  upgrimtrls  48229  gpgprismgr4cycllem11  48428  opmpoismgm  48490  mgmplusgiopALT  48517  2zlidl  48563  rhmsubcALTV  48608  srhmsubcALTV  48648  fldhmsubcALTV  48656  lindslinindsimp1  48780  1arymaptf1  48965  2arymaptf1  48976  eqfnovd  49188  fmpodg  49191  toslat  49304  catprsc  49335  catprsc2  49336  oppcendc  49340  invfn  49352  iinfssclem2  49377  iinfssc  49379  iinfsubc  49380  discsubc  49386  nelsubclem  49389  resccatlem  49395  funchomf  49419  imasubclem2  49427  imaidfu  49432  imasubc  49473  imassc  49475  imasubc3  49478  fthcomf  49479  idfth  49480  cofidfth  49484  upeu2  49494  isnatd  49545  swapfffth  49605  diag1f1  49629  diag2f1  49631  fucoppc  49732  isthincd  49758  isthincd2  49759  oppcthinco  49761  oppcthinendcALT  49763  functhinclem4  49769  functhincfun  49771  thincfth  49774  thincciso  49775  thinccisod  49776  functermc  49830  arweuthinc  49851  arweutermc  49852  diagffth  49860  funcsn  49863  0fucterm  49865