Theorem ralrimivva 3181

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 3179	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  5075  disjxiun  5083  otsndisj  5471  otiunsndisj  5472  swopo  5547  issod  5571  reuop  6255  fcof1  7239  fliftfund  7265  isof1oidb  7276  isof1oopb  7277  soisores  7279  soisoi  7280  isocnv  7282  f1oiso  7303  oveqrspc2v  7391  oprres  7532  caovclg  7556  caovcomg  7559  off  7646  coof  7652  caofidlcan  7666  caofrss  7667  caonncan  7672  dmmpog  8024  fnmpoovd  8034  fmpoco  8042  fsplitfpar  8065  poxp  8075  fvmpocurryd  8218  smo11  8301  smoiso2  8306  omsmo  8591  nnasmo  8596  coflton  8604  qsdisj2  8739  eroprf  8759  dom2lem  8936  omxpenlem  9013  xpf1o  9074  unxpdomlem3  9165  fofinf1o  9239  dffi3  9341  supmo  9362  infmo  9407  inf3lem6  9551  cantnf  9611  rankxplim  9800  fseqenlem1  9943  fodomacn  9975  iunfictbso  10033  cofsmo  10188  infpssrlem5  10226  enfin2i  10240  fin23lem23  10245  fin23lem27  10247  fin23lem28  10259  compssiso  10293  ltordlem  11672  cju  12152  axdc4uzlem  13942  seqcaopr2  13997  seqhomo  14008  wrd2ind  14682  cshf1  14769  s3sndisj  14926  s3iunsndisj  14927  climcn2  15552  addcn2  15553  mulcn2  15555  o1of2  15572  isercolllem1  15624  fsum2dlem  15729  fsumcom2  15733  fprodser  15911  fprod2dlem  15942  fprodcom2  15946  isprm6  16681  crth  16745  eulerthlem2  16749  vdwlem12  16960  cshwsdisj  17066  imasaddfnlem  17489  imasvscafn  17498  mreexexd  17611  iscatd  17636  oppccomfpropd  17690  isofn  17739  sectmon  17746  ssctr  17789  ssceq  17790  catsubcat  17803  issubc3  17813  fullsubc  17814  fullresc  17815  isfuncd  17829  idfucl  17845  cofucl  17852  funcres2b  17861  fulloppc  17888  fthoppc  17889  idffth  17899  cofull  17900  cofth  17901  ressffth  17904  setcmon  18051  setcepi  18052  resssetc  18056  resscatc  18073  catciso  18075  fthestrcsetc  18113  fullestrcsetc  18114  embedsetcestrclem  18120  fthsetcestrc  18128  fullsetcestrc  18129  evlfcl  18185  uncfcurf  18202  hofcl  18222  yonedalem3  18243  yonedainv  18244  yonffthlem  18245  yoniso  18248  isdrs2  18269  isposd  18285  pospropd  18288  poslubmo  18372  posglbmo  18373  chnpof1  18593  mgmplusf  18615  ismgmd  18617  issstrmgm  18618  opifismgm  18624  mgmhmpropd  18663  mgmhmf1o  18665  idmgmhm  18666  issubmgm2  18668  rabsubmgmd  18669  resmgmhm  18676  resmgmhm2  18677  resmgmhm2b  18678  mgmhmco  18679  submgmacs  18682  issgrpd  18695  sgrppropd  18696  ismndd  18721  mndpropd  18724  issubmnd  18726  mndinvmod  18729  ismhmd  18751  mhmpropd  18757  idmhm  18760  mhmf1o  18761  issubmd  18771  mndissubm  18772  0mhm  18784  resmhm  18785  resmhm2  18786  resmhm2b  18787  mhmco  18788  submacs  18792  prdspjmhm  18794  pwsdiagmhm  18796  pwsco1mhm  18797  pwsco2mhm  18798  gsumwspan  18811  frmdsssubm  18826  frmdup1  18829  grpsubf  18992  dfgrp3  19012  mhmmnd  19037  mhmfmhm  19038  issubg4  19118  grpissubg  19119  isnsg3  19132  nsgacs  19134  0nsg  19141  nsgid  19142  qus0subgadd  19171  cycsubmcom  19176  isghmd  19197  ghmmhm  19198  idghm  19203  ghmnsgima  19212  ghmnsgpreima  19213  ghmf1  19218  kerf1ghm  19219  ghmf1o  19220  gaid  19271  subgga  19272  gass  19273  gasubg  19274  cntzsgrpcl  19306  cntzsubm  19310  cntrsubgnsg  19315  lactghmga  19377  symgfixf1  19409  odf1  19534  sylow1lem2  19571  sylow2blem2  19593  sylow3lem1  19599  lsmssv  19615  smndlsmidm  19628  pj1eu  19668  efglem  19688  efgtf  19694  efgred  19720  efgredeu  19724  frgpmhm  19737  frgpuptf  19742  frgpuplem  19744  mulgmhm  19799  ghmcmn  19803  invghm  19805  ablnsg  19819  imasabl  19848  cygabl  19863  gsum2d2lem  19945  gsum2d2  19946  gsumcom2  19947  dprd2d2  20018  ablfaclem2  20060  srgfcl  20174  srgcom4lem  20191  srglmhm  20199  srgrmhm  20200  ringcomlem  20257  isrnghm2d  20427  c0mgm  20436  c0mhm  20437  isrhm2d  20463  subrngringnsg  20527  issubrng2  20532  subrngint  20534  issubrg2  20566  subrgint  20569  rnghmsscmap2  20603  rnghmsscmap  20604  rnghmsubcsetclem2  20606  rhmsscmap2  20632  rhmsscmap  20633  rhmsubcsetclem2  20635  rhmsscrnghm  20639  rhmsubcrngclem2  20641  srhmsubc  20654  rhmsubc  20663  fldhmsubc  20759  primefld  20779  abvn0b  20810  suborng  20850  islmodd  20858  lmodscaf  20876  lmodprop2d  20916  islssd  20927  islss4  20954  lssacs  20959  lsspropd  21010  islmhmd  21032  lmhmima  21040  lmhmpreima  21041  reslmhm  21045  lspextmo  21049  lsmcl  21076  pj1lmhm  21093  islbs2  21150  issubrgd  21182  dflidl2rng  21214  rnglidlmmgm  21241  rhmpreimaidl  21273  rngqiprnglin  21298  expmhm  21432  nn0srg  21433  prmirredlem  21468  expghm  21471  mulgghm2  21472  domnchr  21528  znf1o  21547  zntoslem  21552  znfld  21556  cygznlem3  21565  phlipf  21648  dsmmlss  21740  uvcf1  21788  frlmlbs  21793  lindff1  21816  lindfrn  21817  f1lindf  21818  issubassa2  21888  mvrf1  21980  mplsubglem  21993  mplsubrg  21999  mplcoe5lem  22033  mplcoe2  22035  mplind  22064  evlslem2  22073  evlseu  22077  mhplss  22137  ply1sclf1  22270  evls1maplmhm  22358  mamucl  22382  mamuass  22383  mamudi  22384  mamudir  22385  mamuvs1  22386  mamuvs2  22387  matbas2d  22404  mamumat1cl  22420  mamulid  22422  mamurid  22423  mat1mhm  22465  dmatid  22476  dmatsubcl  22479  dmatsgrp  22480  dmatmulcl  22481  dmatsrng  22482  dmatcrng  22483  scmatscmiddistr  22489  scmatscm  22494  scmatsgrp  22500  scmatsrng  22501  scmatcrng  22502  scmatsgrp1  22503  scmatsrng1  22504  scmatf1  22512  scmatmhm  22515  mavmul0g  22534  mdet1  22582  mdetunilem9  22601  mdetuni0  22602  mdetmul  22604  madutpos  22623  smadiadetlem4  22650  1elcpmat  22696  cpmatacl  22697  cpmatmcl  22700  mat2pmatf1  22710  mat2pmatmul  22712  mat2pmat1  22713  mat2pmatlin  22716  m2cpm  22722  m2cpminvid  22734  m2cpminvid2  22736  decpmatmul  22753  pmatcollpw1  22757  monmatcollpw  22760  pmatcollpw  22762  pmatcollpw3lem  22764  pmatcollpwscmatlem2  22771  pm2mpf1  22780  mp2pm2mplem4  22790  pm2mpmhmlem2  22800  chp0mat  22827  chpidmat  22828  tgclb  22951  mretopd  23073  toponmre  23074  iscldtop  23076  ordtbaslem  23169  ordtbas2  23172  cnt0  23327  haust1  23333  cnhaus  23335  isreg2  23358  dishaus  23363  ordthaus  23365  dfconn2  23400  iunconn  23409  clsconn  23411  2ndcomap  23439  dis2ndc  23441  llynlly  23458  restnlly  23463  restlly  23464  islly2  23465  llyidm  23469  nllyidm  23470  hausllycmp  23475  kgentopon  23519  txbas  23548  ptbasin2  23559  ptbasfi  23562  txcnp  23601  txcnmpt  23605  pthaus  23619  tx1stc  23631  xkococnlem  23640  xkococn  23641  cnmpt21  23652  qtoptop2  23680  qtopeu  23697  kqt0lem  23717  isr0  23718  regr1lem2  23721  kqreglem1  23722  kqreglem2  23723  kqnrmlem1  23724  kqnrmlem2  23725  nrmr0reg  23730  reghmph  23774  nrmhmph  23775  txswaphmeo  23786  qtophmeo  23798  fbun  23821  trfbas2  23824  isfil2  23837  infil  23844  trfil2  23868  filssufilg  23892  hausflim  23962  fclsnei  24000  fclsfnflim  24008  flimfnfcls  24009  ptcmplem1  24033  clssubg  24090  tgpconncomp  24094  qustgplem  24102  tsmsfbas  24109  utoptop  24215  iducn  24263  cstucnd  24264  isxmetd  24307  isxmet2d  24308  xmettpos  24330  prdsdsf  24348  prdsmet  24351  ressprdsds  24352  imasdsf1olem  24354  imasf1oxmet  24356  imasf1omet  24357  blfvalps  24364  xmetresbl  24418  metss2  24493  comet  24494  stdbdmet  24497  stdbdmopn  24499  methaus  24501  met2ndci  24503  metustfbas  24538  nrmmetd  24555  subgngp  24616  ngptgp  24617  sranlm  24665  nlmvscnlem1  24667  nlmvscn  24668  nrginvrcn  24673  lssnlm  24682  nghmcn  24726  qtopbaslem  24739  reconn  24810  xmetdcn2  24819  metdscn  24838  metnrm  24844  elcncf1di  24878  cncfcdm  24881  mulc1cncf  24888  cncfco  24890  reparphti  24980  isncvsngpd  25133  tcphcph  25220  ipcnlem1  25228  ipcn  25229  iscfil3  25256  bcthlem5  25311  rrxmet  25391  minveclem3  25412  minveclem7  25418  ovolicc2lem4  25503  dyadmbl  25583  volcn  25589  itg1addlem1  25675  itg1addlem2  25680  itg1addlem4  25682  mbfi1fseqlem1  25698  mbfi1fseqlem3  25700  mbfi1fseqlem4  25701  mbfi1fseqlem5  25702  dvmptfsum  25958  c1liplem1  25979  dvgt0lem2  25986  ftc1a  26020  ply1domn  26105  ply1divmo  26117  fta1b  26153  ig1peu  26156  coeeu  26206  plydivalg  26282  aaliou2b  26324  ulmss  26381  ulmcn  26383  efif1olem4  26528  efsubm  26534  logccv  26646  logbmpt  26771  logbfval  26773  cvxcl  26968  basellem4  27067  fsumdvdscom  27168  musum  27174  mpodvdsmulf1o  27177  fsumdvdsmul  27178  dvdsmulf1o  27179  dchrelbasd  27222  dchrmulcl  27232  dchrinv  27244  lgsqrlem2  27330  lgsdchr  27338  lgseisenlem2  27359  lgsquadlem1  27363  lgsquadlem2  27364  2sqreulem4  27437  dchrisumlema  27471  dchrisumlem2  27473  chpdifbndlem2  27537  pntpbnd  27571  pntibndlem3  27575  sltsd  27780  oldbday  27913  addsprop  27988  mulcutlem  28143  divsmo  28196  om2noseqf1o  28313  om2noseqiso  28314  axtgcont  28557  tgjustc1  28563  tgjustc2  28564  iscgrglt  28602  ercgrg  28605  idmot  28625  motco  28628  cnvmot  28629  motcgrg  28632  tgisline  28715  tghilberti2  28726  mirreu3  28742  mirmot  28763  ragperp  28805  foot  28810  mideu  28826  midf  28864  lmimot  28886  trgcopyeu  28894  f1otrgds  28957  f1otrg  28959  f1otrge  28960  xmstrkgc  28974  brbtwn2  28994  axlowdimlem15  29045  axcontlem2  29054  axcontlem10  29062  eengtrkg  29075  eengtrkge  29076  numedglnl  29233  usgredgreu  29307  uspgredg2vtxeu  29309  uspgredg2v  29313  usgredg2v  29316  wlkswwlksf1o  29968  wwlksnextinj  29988  clwlkclwwlkf1  30101  clwwlkf1  30140  frcond4  30361  frgrncvvdeqlem8  30397  frgrncvvdeq  30400  frgrwopreglem4  30406  numclwwlk1lem2f1  30448  nrt2irr  30564  grpoinvf  30624  nvmf  30737  vacn  30786  nmcvcn  30787  smcnlem  30789  sspg  30820  ssps  30822  sspmlem  30824  0lno  30882  blocni  30897  ipblnfi  30947  minvecolem7  30975  unopf1o  32008  cnvunop  32010  unoplin  32012  counop  32013  hmopadj2  32033  hmoplin  32034  bralnfn  32040  lnopeq0i  32099  hmops  32112  hmopm  32113  hmopco  32115  lnconi  32125  cnlnadjlem2  32160  adjmul  32184  adjadd  32185  cdjreui  32524  disjxpin  32679  off2  32735  2ndresdju  32743  fnpreimac  32764  suppovss  32775  f1od2  32813  xrofsup  32861  s3f1  33028  ccatf1  33030  swrdf1  33037  odutos  33049  dfmgc2lem  33076  dfmgc2  33077  pwrssmgc  33081  mgcf1o  33084  mndlactf1  33107  mndractf1  33109  abliso  33117  symgcntz  33167  tocyccntz  33226  conjga  33252  fxpsubrg  33256  archiabllem1  33275  archiabllem2  33279  urpropd  33313  elrgspnlem2  33325  rlocf1  33355  rrgsubm  33366  subrdom  33367  xrge0slmod  33429  nsgmgc  33493  intlidl  33501  idlinsubrg  33512  rhmimaidl  33513  prmidl2  33522  idlmulssprm  33523  isprmidlc  33528  rhmpreimaprmidl  33532  qsidomlem1  33533  qsidomlem2  33534  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  ssmxidllem  33554  rsprprmprmidl  33603  rsprprmprmidlb  33604  rprmirred  33612  rprmirredb  33613  1arithufdlem4  33628  extvfvcl  33701  mplvrpmga  33710  ply1degltdimlem  33788  ply1degltdim  33789  lindsun  33791  fedgmullem1  33795  fedgmullem2  33796  fedgmul  33797  lactlmhm  33800  assalactf1o  33801  minplyirred  33877  constrsdrg  33941  1smat1  33970  submateq  33975  madjusmdetlem3  33995  zart0  34045  pstmxmet  34063  ofcf  34269  ldgenpisys  34332  rossros  34346  inelcarsg  34477  sibfof  34506  sitmf  34518  hgt750lemb  34822  erdszelem4  35398  erdszelem9  35403  erdsze2lem2  35408  cnpconn  35434  pconnconn  35435  txpconn  35436  ptpconn  35437  cvxpconn  35446  cvxsconn  35447  iccllysconn  35454  cvmseu  35480  cvmliftmo  35488  cvmlift2lem5  35511  cvmlift2lem9  35515  mrsubff1  35718  elmrsubrn  35724  mrsubco  35725  msubff1  35760  mvhf1  35763  r1peuqusdeg1  35847  segconeu  36215  fnessref  36561  neibastop1  36563  filnetlem3  36584  onsuct0  36645  weiunlem  36667  mh-inf3f1  36745  unblimceq0lem  36788  unbdqndv2  36793  knoppndv  36816  irrdiff  37662  uncf  37942  fin2so  37950  lindsadd  37956  poimirlem4  37967  poimirlem13  37976  poimirlem14  37977  poimirlem26  37989  heicant  37998  mblfinlem2  38001  ftc1anc  38044  sdclem1  38086  isbnd3  38127  prdsbnd  38136  ismtycnv  38145  ismtyhmeolem  38147  ismtyres  38151  bfplem1  38165  bfplem2  38166  bfp  38167  rrnmet  38172  ismrer1  38181  iccbnd  38183  grpokerinj  38236  isdrngo2  38301  rngogrphom  38314  rngohomco  38317  rngoisocnv  38324  iscringd  38341  eqvreldisj1  39270  erprt  39341  lfl0f  39537  lkrlss  39563  lshpsmreu  39577  linepsubN  40220  pmapsub  40236  lautcnv  40558  lautco  40565  idltrn  40618  cdleme50f1  41011  cdleme50laut  41015  istendod  41230  dihf11  41735  dih1dimatlem  41797  lcfl7N  41969  lcfrlem9  42018  mapd1o  42116  hdmapf1oN  42333  hgmapf1oN  42371  fmpocos  42697  qsalrel  42702  rediveud  42897  imacrhmcl  42981  evlselv  43042  fsuppind  43045  nacsfix  43166  rmxypairf1o  43365  wepwsolem  43496  dnnumch3  43501  fnwe2  43507  mpaaeu  43604  idomsubgmo  43647  mon1psubm  43653  deg1mhm  43654  isotone1  44501  isotone2  44502  mnringmulrcld  44681  traxext  45430  disjxp1  45526  disjf1  45639  wessf1ornlem  45641  projf1o  45652  sumnnodd  46086  lptioo2  46087  lptioo1  46088  cncfshift  46328  cncfperiod  46333  dvnprodlem1  46400  fourierdlem42  46603  nnfoctbdjlem  46909  isomennd  46985  smflimlem6  47230  fsetsnf1  47520  cfsetsnfsetf1  47527  otiunsndisjX  47747  imasetpreimafvbijlemf1  47884  iccpartgt  47907  icceuelpart  47916  ichnreuop  47952  sprsymrelfolem2  47973  sprsymrelf  47975  prproropf1o  47987  reupr  48002  reuopreuprim  48006  uhgrimprop  48388  isuspgrim0lem  48389  upgrimtrls  48402  gpgprismgr4cycllem11  48601  opmpoismgm  48663  mgmplusgiopALT  48690  2zlidl  48736  rhmsubcALTV  48781  srhmsubcALTV  48821  fldhmsubcALTV  48829  lindslinindsimp1  48953  1arymaptf1  49138  2arymaptf1  49149  eqfnovd  49361  fmpodg  49364  toslat  49477  catprsc  49508  catprsc2  49509  oppcendc  49513  invfn  49525  iinfssclem2  49550  iinfssc  49552  iinfsubc  49553  discsubc  49559  nelsubclem  49562  resccatlem  49568  funchomf  49592  imasubclem2  49600  imaidfu  49605  imasubc  49646  imassc  49648  imasubc3  49651  fthcomf  49652  idfth  49653  cofidfth  49657  upeu2  49667  isnatd  49718  swapfffth  49778  diag1f1  49802  diag2f1  49804  fucoppc  49905  isthincd  49931  isthincd2  49932  oppcthinco  49934  oppcthinendcALT  49936  functhinclem4  49942  functhincfun  49944  thincfth  49947  thincciso  49948  thinccisod  49949  functermc  50003  arweuthinc  50024  arweutermc  50025  diagffth  50033  funcsn  50036  0fucterm  50038