Theorem ralrimivva 3201

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

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 398  df-ral 3063

This theorem is referenced by:  disjord  5136  disjxiun  5145  otsndisj  5519  otiunsndisj  5520  swopo  5599  issod  5621  reuop  6290  fcof1  7282  fliftfund  7307  isof1oidb  7318  isof1oopb  7319  soisores  7321  soisoi  7322  isocnv  7324  f1oiso  7345  oveqrspc2v  7433  oprres  7572  caovclg  7596  caovcomg  7599  off  7685  caofrss  7703  caonncan  7708  dmmpog  8058  fnmpoovd  8070  fmpoco  8078  fsplitfpar  8101  poxp  8111  fvmpocurryd  8253  smo11  8361  smoiso2  8366  omsmo  8654  nnasmo  8659  coflton  8667  qsdisj2  8786  eroprf  8806  dom2lem  8985  omxpenlem  9070  xpf1o  9136  unxpdomlem3  9249  fofinf1o  9324  dffi3  9423  supmo  9444  infmo  9487  inf3lem6  9625  cantnf  9685  rankxplim  9871  fseqenlem1  10016  fodomacn  10048  iunfictbso  10106  cofsmo  10261  infpssrlem5  10299  enfin2i  10313  fin23lem23  10318  fin23lem27  10320  fin23lem28  10332  compssiso  10366  ltordlem  11736  cju  12205  axdc4uzlem  13945  seqcaopr2  14001  seqhomo  14012  wrd2ind  14670  cshf1  14757  s3sndisj  14911  s3iunsndisj  14912  climcn2  15534  addcn2  15535  mulcn2  15537  o1of2  15554  isercolllem1  15608  fsum2dlem  15713  fsumcom2  15717  fprodser  15890  fprod2dlem  15921  fprodcom2  15925  isprm6  16648  crth  16708  eulerthlem2  16712  vdwlem12  16922  cshwsdisj  17029  imasaddfnlem  17471  imasvscafn  17480  mreexexd  17589  iscatd  17614  oppccomfpropd  17670  isofn  17719  sectmon  17726  ssctr  17769  ssceq  17770  catsubcat  17786  issubc3  17796  fullsubc  17797  fullresc  17798  isfuncd  17812  idfucl  17828  cofucl  17835  funcres2b  17844  fulloppc  17870  fthoppc  17871  idffth  17881  cofull  17882  cofth  17883  ressffth  17886  setcmon  18034  setcepi  18035  resssetc  18039  resscatc  18056  catciso  18058  fthestrcsetc  18099  fullestrcsetc  18100  embedsetcestrclem  18106  fthsetcestrc  18114  fullsetcestrc  18115  evlfcl  18172  uncfcurf  18189  hofcl  18209  yonedalem3  18230  yonedainv  18231  yonffthlem  18232  yoniso  18235  isdrs2  18256  isposd  18273  pospropd  18277  poslubmo  18361  posglbmo  18362  mgmplusf  18568  issstrmgm  18569  opifismgm  18575  issgrpd  18618  sgrppropd  18619  ismndd  18644  mndpropd  18647  issubmnd  18649  mndinvmod  18652  ismhmd  18671  mhmpropd  18675  idmhm  18678  mhmf1o  18679  issubmd  18684  mndissubm  18685  0mhm  18697  resmhm  18698  resmhm2  18699  resmhm2b  18700  mhmco  18701  submacs  18705  prdspjmhm  18707  pwsdiagmhm  18709  pwsco1mhm  18710  pwsco2mhm  18711  gsumwspan  18724  frmdsssubm  18739  frmdup1  18742  grpsubf  18899  dfgrp3  18919  mhmmnd  18942  mhmfmhm  18943  issubg4  19020  grpissubg  19021  isnsg3  19035  nsgacs  19037  0nsg  19044  nsgid  19045  qus0subgadd  19071  cycsubmcom  19076  isghmd  19096  ghmmhm  19097  idghm  19102  ghmnsgima  19111  ghmnsgpreima  19112  ghmf1  19116  ghmf1o  19117  gaid  19158  subgga  19159  gass  19160  gasubg  19161  cntzsgrpcl  19193  cntzsubm  19197  cntrsubgnsg  19202  lactghmga  19268  symgfixf1  19300  odf1  19425  sylow1lem2  19462  sylow2blem2  19484  sylow3lem1  19490  lsmssv  19506  smndlsmidm  19519  pj1eu  19559  efglem  19579  efgtf  19585  efgred  19611  efgredeu  19615  frgpmhm  19628  frgpuptf  19633  frgpuplem  19635  mulgmhm  19690  ghmcmn  19694  invghm  19696  ablnsg  19710  imasabl  19739  cygabl  19754  gsum2d2lem  19836  gsum2d2  19837  gsumcom2  19838  dprd2d2  19909  ablfaclem2  19951  srgfcl  20013  srgcom4lem  20030  srglmhm  20038  srgrmhm  20039  ringcomlem  20090  isrhm2d  20258  kerf1ghm  20275  issubrg2  20376  subrgint  20379  primefld  20414  islmodd  20470  lmodscaf  20487  lmodprop2d  20527  islssd  20539  islss4  20566  lssacs  20571  lsspropd  20621  islmhmd  20643  lmhmima  20651  lmhmpreima  20652  reslmhm  20656  lspextmo  20660  lsmcl  20687  pj1lmhm  20704  islbs2  20760  issubrgd  20804  dflidl2  20836  opprdomn  20912  abvn0b  20913  expmhm  21007  nn0srg  21008  prmirredlem  21034  expghm  21037  mulgghm2  21038  domnchr  21076  znf1o  21099  zntoslem  21104  znfld  21108  cygznlem3  21117  phlipf  21197  dsmmlss  21291  uvcf1  21339  frlmlbs  21344  lindff1  21367  lindfrn  21368  f1lindf  21369  issubassa2  21438  mvrf1  21537  mplsubglem  21550  mplsubrg  21556  mplcoe5lem  21586  mplcoe2  21588  mplind  21623  evlslem2  21634  evlseu  21638  mhplss  21690  ply1sclf1  21803  mamucl  21893  mamuass  21894  mamudi  21895  mamudir  21896  mamuvs1  21897  mamuvs2  21898  matbas2d  21917  mamumat1cl  21933  mamulid  21935  mamurid  21936  mat1mhm  21978  dmatid  21989  dmatsubcl  21992  dmatsgrp  21993  dmatmulcl  21994  dmatsrng  21995  dmatcrng  21996  scmatscmiddistr  22002  scmatscm  22007  scmatsgrp  22013  scmatsrng  22014  scmatcrng  22015  scmatsgrp1  22016  scmatsrng1  22017  scmatf1  22025  scmatmhm  22028  mavmul0g  22047  mdet1  22095  mdetunilem9  22114  mdetuni0  22115  mdetmul  22117  madutpos  22136  smadiadetlem4  22163  1elcpmat  22209  cpmatacl  22210  cpmatmcl  22213  mat2pmatf1  22223  mat2pmatmul  22225  mat2pmat1  22226  mat2pmatlin  22229  m2cpm  22235  m2cpminvid  22247  m2cpminvid2  22249  decpmatmul  22266  pmatcollpw1  22270  monmatcollpw  22273  pmatcollpw  22275  pmatcollpw3lem  22277  pmatcollpwscmatlem2  22284  pm2mpf1  22293  mp2pm2mplem4  22303  pm2mpmhmlem2  22313  chp0mat  22340  chpidmat  22341  tgclb  22465  mretopd  22588  toponmre  22589  iscldtop  22591  ordtbaslem  22684  ordtbas2  22687  cnt0  22842  haust1  22848  cnhaus  22850  isreg2  22873  dishaus  22878  ordthaus  22880  dfconn2  22915  iunconn  22924  clsconn  22926  2ndcomap  22954  dis2ndc  22956  llynlly  22973  restnlly  22978  restlly  22979  islly2  22980  llyidm  22984  nllyidm  22985  hausllycmp  22990  kgentopon  23034  txbas  23063  ptbasin2  23074  ptbasfi  23077  txcnp  23116  txcnmpt  23120  pthaus  23134  tx1stc  23146  xkococnlem  23155  xkococn  23156  cnmpt21  23167  qtoptop2  23195  qtopeu  23212  kqt0lem  23232  isr0  23233  regr1lem2  23236  kqreglem1  23237  kqreglem2  23238  kqnrmlem1  23239  kqnrmlem2  23240  nrmr0reg  23245  reghmph  23289  nrmhmph  23290  txswaphmeo  23301  qtophmeo  23313  fbun  23336  trfbas2  23339  isfil2  23352  infil  23359  trfil2  23383  filssufilg  23407  hausflim  23477  fclsnei  23515  fclsfnflim  23523  flimfnfcls  23524  ptcmplem1  23548  clssubg  23605  tgpconncomp  23609  qustgplem  23617  tsmsfbas  23624  utoptop  23731  iducn  23780  cstucnd  23781  isxmetd  23824  isxmet2d  23825  xmettpos  23847  prdsdsf  23865  prdsmet  23868  ressprdsds  23869  imasdsf1olem  23871  imasf1oxmet  23873  imasf1omet  23874  blfvalps  23881  xmetresbl  23935  metss2  24013  comet  24014  stdbdmet  24017  stdbdmopn  24019  methaus  24021  met2ndci  24023  metustfbas  24058  nrmmetd  24075  subgngp  24136  ngptgp  24137  sranlm  24193  nlmvscnlem1  24195  nlmvscn  24196  nrginvrcn  24201  lssnlm  24210  nghmcn  24254  qtopbaslem  24267  reconn  24336  xmetdcn2  24345  metdscn  24364  metnrm  24370  elcncf1di  24403  cncfcdm  24406  mulc1cncf  24413  cncfco  24415  reparphti  24505  isncvsngpd  24659  tcphcph  24746  ipcnlem1  24754  ipcn  24755  iscfil3  24782  bcthlem5  24837  rrxmet  24917  minveclem3  24938  minveclem7  24944  ovolicc2lem4  25029  dyadmbl  25109  volcn  25115  itg1addlem1  25201  itg1addlem2  25206  itg1addlem4  25208  itg1addlem4OLD  25209  mbfi1fseqlem1  25225  mbfi1fseqlem3  25227  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  dvmptfsum  25484  c1liplem1  25505  dvgt0lem2  25512  ftc1a  25546  ply1domn  25633  ply1divmo  25645  fta1b  25679  ig1peu  25681  coeeu  25731  plydivalg  25804  aaliou2b  25846  ulmss  25901  ulmcn  25903  efif1olem4  26046  efsubm  26052  logccv  26163  logbmpt  26283  logbfval  26285  cvxcl  26479  basellem4  26578  fsumdvdscom  26679  musum  26685  dvdsmulf1o  26688  fsumdvdsmul  26689  dchrelbasd  26732  dchrmulcl  26742  dchrinv  26754  lgsqrlem2  26840  lgsdchr  26848  lgseisenlem2  26869  lgsquadlem1  26873  lgsquadlem2  26874  2sqreulem4  26947  dchrisumlema  26981  dchrisumlem2  26983  chpdifbndlem2  27047  pntpbnd  27081  pntibndlem3  27085  ssltd  27283  oldbday  27385  addsprop  27450  mulscutlem  27577  divsmo  27624  axtgcont  27710  tgjustc1  27716  tgjustc2  27717  iscgrglt  27755  ercgrg  27758  idmot  27778  motco  27781  cnvmot  27782  motcgrg  27785  tgisline  27868  tghilberti2  27879  mirreu3  27895  mirmot  27916  ragperp  27958  foot  27963  mideu  27979  midf  28017  lmimot  28039  trgcopyeu  28047  f1otrgds  28110  f1otrg  28112  f1otrge  28113  xmstrkgc  28133  brbtwn2  28153  axlowdimlem15  28204  axcontlem2  28213  axcontlem10  28221  eengtrkg  28234  eengtrkge  28235  numedglnl  28394  usgredgreu  28465  uspgredg2vtxeu  28467  uspgredg2v  28471  usgredg2v  28474  wlkswwlksf1o  29123  wwlksnextinj  29143  clwlkclwwlkf1  29253  clwwlkf1  29292  frcond4  29513  frgrncvvdeqlem8  29549  frgrncvvdeq  29552  frgrwopreglem4  29558  numclwwlk1lem2f1  29600  grpoinvf  29773  nvmf  29886  vacn  29935  nmcvcn  29936  smcnlem  29938  sspg  29969  ssps  29971  sspmlem  29973  0lno  30031  blocni  30046  ipblnfi  30096  minvecolem7  30124  unopf1o  31157  cnvunop  31159  unoplin  31161  counop  31162  hmopadj2  31182  hmoplin  31183  bralnfn  31189  lnopeq0i  31248  hmops  31261  hmopm  31262  hmopco  31264  lnconi  31274  cnlnadjlem2  31309  adjmul  31333  adjadd  31334  cdjreui  31673  disjxpin  31807  off2  31854  2ndresdju  31862  fnpreimac  31884  suppovss  31894  f1od2  31934  xrofsup  31968  s3f1  32101  ccatf1  32103  swrdf1  32108  odutos  32126  dfmgc2lem  32153  dfmgc2  32154  pwrssmgc  32158  mgcf1o  32161  abliso  32185  symgcntz  32234  tocyccntz  32291  archiabllem1  32327  archiabllem2  32331  urpropd  32366  suborng  32422  xrge0slmod  32452  nsgmgc  32512  intlidl  32525  rhmpreimaidl  32526  idlinsubrg  32538  rhmimaidl  32539  prmidl2  32548  idlmulssprm  32549  isprmidlc  32555  rhmpreimaprmidl  32559  qsidomlem1  32560  qsidomlem2  32561  mxidlprm  32575  mxidlirredi  32576  ssmxidllem  32578  ply1degltdimlem  32696  ply1degltdim  32697  lindsun  32699  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  evls1maplmhm  32749  minplyirred  32759  1smat1  32773  submateq  32778  madjusmdetlem3  32798  zart0  32848  pstmxmet  32866  ofcf  33090  ldgenpisys  33153  rossros  33167  inelcarsg  33299  sibfof  33328  sitmf  33340  hgt750lemb  33657  erdszelem4  34174  erdszelem9  34179  erdsze2lem2  34184  cnpconn  34210  pconnconn  34211  txpconn  34212  ptpconn  34213  cvxpconn  34222  cvxsconn  34223  iccllysconn  34230  cvmseu  34256  cvmliftmo  34264  cvmlift2lem5  34287  cvmlift2lem9  34291  mrsubff1  34494  elmrsubrn  34500  mrsubco  34501  msubff1  34536  mvhf1  34539  segconeu  34972  gg-reparphti  35161  fnessref  35231  neibastop1  35233  filnetlem3  35254  onsuct0  35315  unblimceq0lem  35371  unbdqndv2  35376  knoppndv  35399  irrdiff  36196  uncf  36456  fin2so  36464  lindsadd  36470  poimirlem4  36481  poimirlem13  36490  poimirlem14  36491  poimirlem26  36503  heicant  36512  mblfinlem2  36515  ftc1anc  36558  sdclem1  36600  isbnd3  36641  prdsbnd  36650  ismtycnv  36659  ismtyhmeolem  36661  ismtyres  36665  bfplem1  36679  bfplem2  36680  bfp  36681  rrnmet  36686  ismrer1  36695  iccbnd  36697  grpokerinj  36750  isdrngo2  36815  rngogrphom  36828  rngohomco  36831  rngoisocnv  36838  iscringd  36855  eqvreldisj1  37683  erprt  37732  lfl0f  37928  lkrlss  37954  lshpsmreu  37968  linepsubN  38612  pmapsub  38628  lautcnv  38950  lautco  38957  idltrn  39010  cdleme50f1  39403  cdleme50laut  39407  istendod  39622  dihf11  40127  dih1dimatlem  40189  lcfl7N  40361  lcfrlem9  40410  mapd1o  40508  hdmapf1oN  40725  hgmapf1oN  40763  fmpocos  41054  qsalrel  41060  imacrhmcl  41087  evlselv  41157  fsuppind  41160  sn-negex12  41286  nacsfix  41436  rmxypairf1o  41636  wepwsolem  41770  dnnumch3  41775  fnwe2  41781  mpaaeu  41878  idomsubgmo  41926  mon1psubm  41934  deg1mhm  41935  isotone1  42785  isotone2  42786  mnringmulrcld  42973  disjxp1  43742  disjf1  43866  wessf1ornlem  43868  projf1o  43882  sumnnodd  44333  lptioo2  44334  lptioo1  44335  cncfshift  44577  cncfperiod  44582  dvnprodlem1  44649  fourierdlem42  44852  nnfoctbdjlem  45158  isomennd  45234  smflimlem6  45479  fsetsnf1  45749  cfsetsnfsetf1  45756  otiunsndisjX  45974  imasetpreimafvbijlemf1  46059  iccpartgt  46082  icceuelpart  46091  ichnreuop  46127  sprsymrelfolem2  46148  sprsymrelf  46150  prproropf1o  46162  reupr  46177  reuopreuprim  46181  isomuspgrlem2c  46485  isomuspgr  46489  ismgmd  46533  mgmhmpropd  46542  mgmhmf1o  46544  idmgmhm  46545  issubmgm2  46547  rabsubmgmd  46548  resmgmhm  46555  resmgmhm2  46556  resmgmhm2b  46557  mgmhmco  46558  submgmacs  46561  opmpoismgm  46564  mgmplusgiopALT  46591  isrnghm2d  46685  c0mgm  46694  c0mhm  46695  subrngringnsg  46717  issubrng2  46722  subrngint  46724  rnglidlmmgm  46739  rngqiprnglin  46768  2zlidl  46786  rnghmsscmap2  46825  rnghmsscmap  46826  rnghmsubcsetclem2  46828  rhmsscmap2  46871  rhmsscmap  46872  rhmsubcsetclem2  46874  rhmsscrnghm  46878  rhmsubcrngclem2  46880  srhmsubc  46928  fldhmsubc  46936  rhmsubc  46942  srhmsubcALTV  46946  fldhmsubcALTV  46954  rhmsubcALTV  46960  lindslinindsimp1  47092  1arymaptf1  47282  2arymaptf1  47293  toslat  47561  catprsc  47587  catprsc2  47588  isthincd  47611  isthincd2  47612  functhinclem4  47618  thincfth  47622  thincciso  47623