Theorem ralrimivva 3191

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  disjord  5054  disjxiun  5063  otsndisj  5409  otiunsndisj  5410  swopo  5484  issod  5506  reuop  6144  fcof1  7043  fliftfund  7066  isof1oidb  7077  isof1oopb  7078  soisores  7080  soisoi  7081  isocnv  7083  f1oiso  7104  oveqrspc2v  7183  oprres  7316  caovclg  7340  caovcomg  7343  off  7424  caofrss  7442  caonncan  7447  dmmpog  7772  fnmpoovd  7782  fmpoco  7790  fsplitfpar  7814  poxp  7822  fvmpocurryd  7937  smo11  8001  smoiso2  8006  omsmo  8281  qsdisj2  8375  eroprf  8395  dom2lem  8549  omxpenlem  8618  xpf1o  8679  unxpdomlem3  8724  fofinf1o  8799  dffi3  8895  supmo  8916  infmo  8959  inf3lem6  9096  cantnf  9156  rankxplim  9308  fseqenlem1  9450  fodomacn  9482  iunfictbso  9540  cofsmo  9691  infpssrlem5  9729  enfin2i  9743  fin23lem23  9748  fin23lem27  9750  fin23lem28  9762  compssiso  9796  ltordlem  11165  cju  11634  axdc4uzlem  13352  seqcaopr2  13407  seqhomo  13418  wrd2ind  14085  cshf1  14172  s3sndisj  14327  s3iunsndisj  14328  climcn2  14949  addcn2  14950  mulcn2  14952  o1of2  14969  isercolllem1  15021  fsum2dlem  15125  fsumcom2  15129  fprodser  15303  fprod2dlem  15334  fprodcom2  15338  isprm6  16058  crth  16115  eulerthlem2  16119  vdwlem12  16328  cshwsdisj  16432  imasaddfnlem  16801  imasvscafn  16810  mreexexd  16919  iscatd  16944  oppccomfpropd  16997  isofn  17045  sectmon  17052  ssctr  17095  ssceq  17096  catsubcat  17109  issubc3  17119  fullsubc  17120  fullresc  17121  isfuncd  17135  idfucl  17151  cofucl  17158  funcres2b  17167  fulloppc  17192  fthoppc  17193  idffth  17203  cofull  17204  cofth  17205  ressffth  17208  setcmon  17347  setcepi  17348  resssetc  17352  resscatc  17365  catciso  17367  fthestrcsetc  17400  fullestrcsetc  17401  embedsetcestrclem  17407  fthsetcestrc  17415  fullsetcestrc  17416  evlfcl  17472  uncfcurf  17489  hofcl  17509  yonedalem3  17530  yonedainv  17531  yonffthlem  17532  yoniso  17535  isdrs2  17549  isposd  17565  pospropd  17744  poslubmo  17756  posglbmo  17757  mgmplusf  17862  issstrmgm  17863  opifismgm  17869  ismndd  17933  mndpropd  17936  issubmnd  17938  mndinvmod  17941  mhmpropd  17962  idmhm  17965  mhmf1o  17966  issubmd  17971  mndissubm  17972  0mhm  17984  resmhm  17985  resmhm2  17986  resmhm2b  17987  mhmco  17988  submacs  17991  prdspjmhm  17993  pwsdiagmhm  17995  pwsco1mhm  17996  pwsco2mhm  17997  gsumwspan  18011  frmdsssubm  18026  frmdup1  18029  grpsubf  18178  dfgrp3  18198  mhmmnd  18221  mhmfmhm  18222  issubg4  18298  grpissubg  18299  isnsg3  18312  nsgacs  18314  0nsg  18321  nsgid  18322  cycsubmcom  18347  isghmd  18367  ghmmhm  18368  idghm  18373  ghmnsgima  18382  ghmnsgpreima  18383  ghmf1  18387  ghmf1o  18388  gaid  18429  subgga  18430  gass  18431  gasubg  18432  cntzsubm  18466  cntrsubgnsg  18471  lactghmga  18533  symgfixf1  18565  odf1  18689  sylow1lem2  18724  sylow2blem2  18746  sylow3lem1  18752  lsmssv  18768  smndlsmidm  18781  lsmidmOLD  18789  pj1eu  18822  efglem  18842  efgtf  18848  efgred  18874  efgredeu  18878  frgpmhm  18891  frgpuptf  18896  frgpuplem  18898  mulgmhm  18948  ghmcmn  18952  invghm  18954  ablnsg  18967  cygabl  19010  gsum2d2lem  19093  gsum2d2  19094  gsumcom2  19095  dprd2d2  19166  ablfaclem2  19208  srgfcl  19265  srglmhm  19285  srgrmhm  19286  isrhm2d  19480  kerf1ghm  19497  kerf1hrmOLD  19498  issubrg2  19555  subrgint  19557  primefld  19584  islmodd  19640  lmodscaf  19656  lmodprop2d  19696  islssd  19707  islss4  19734  lssacs  19739  lsspropd  19789  islmhmd  19811  lmhmima  19819  lmhmpreima  19820  reslmhm  19824  lspextmo  19828  lsmcl  19855  pj1lmhm  19872  islbs2  19926  issubrngd2  19961  opprdomn  20074  abvn0b  20075  issubassa2  20121  mvrf1  20205  mplsubglem  20214  mplsubrg  20220  mplcoe5lem  20248  mplcoe2  20250  mplind  20282  evlslem2  20292  evlseu  20296  mhplss  20342  ply1sclf1  20457  expmhm  20614  nn0srg  20615  prmirredlem  20640  expghm  20643  mulgghm2  20644  domnchr  20679  znf1o  20698  zntoslem  20703  znfld  20707  cygznlem3  20716  phlipf  20796  dsmmlss  20888  uvcf1  20936  frlmlbs  20941  lindff1  20964  lindfrn  20965  f1lindf  20966  mamucl  21010  mamuass  21011  mamudi  21012  mamudir  21013  mamuvs1  21014  mamuvs2  21015  matbas2d  21032  mamumat1cl  21048  mamulid  21050  mamurid  21051  mat1mhm  21093  dmatid  21104  dmatsubcl  21107  dmatsgrp  21108  dmatmulcl  21109  dmatsrng  21110  dmatcrng  21111  scmatscmiddistr  21117  scmatscm  21122  scmatsgrp  21128  scmatsrng  21129  scmatcrng  21130  scmatsgrp1  21131  scmatsrng1  21132  scmatf1  21140  scmatmhm  21143  mavmul0g  21162  mdet1  21210  mdetunilem9  21229  mdetuni0  21230  mdetmul  21232  madutpos  21251  smadiadetlem4  21278  1elcpmat  21323  cpmatacl  21324  cpmatmcl  21327  mat2pmatf1  21337  mat2pmatmul  21339  mat2pmat1  21340  mat2pmatlin  21343  m2cpm  21349  m2cpminvid  21361  m2cpminvid2  21363  decpmatmul  21380  pmatcollpw1  21384  monmatcollpw  21387  pmatcollpw  21389  pmatcollpw3lem  21391  pmatcollpwscmatlem2  21398  pm2mpf1  21407  mp2pm2mplem4  21417  pm2mpmhmlem2  21427  chp0mat  21454  chpidmat  21455  tgclb  21578  mretopd  21700  toponmre  21701  iscldtop  21703  ordtbaslem  21796  ordtbas2  21799  cnt0  21954  haust1  21960  cnhaus  21962  isreg2  21985  dishaus  21990  ordthaus  21992  dfconn2  22027  iunconn  22036  clsconn  22038  2ndcomap  22066  dis2ndc  22068  llynlly  22085  restnlly  22090  restlly  22091  islly2  22092  llyidm  22096  nllyidm  22097  hausllycmp  22102  kgentopon  22146  txbas  22175  ptbasin2  22186  ptbasfi  22189  txcnp  22228  txcnmpt  22232  pthaus  22246  tx1stc  22258  xkococnlem  22267  xkococn  22268  cnmpt21  22279  qtoptop2  22307  qtopeu  22324  kqt0lem  22344  isr0  22345  regr1lem2  22348  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  nrmr0reg  22357  reghmph  22401  nrmhmph  22402  txswaphmeo  22413  qtophmeo  22425  fbun  22448  trfbas2  22451  isfil2  22464  infil  22471  trfil2  22495  filssufilg  22519  hausflim  22589  fclsnei  22627  fclsfnflim  22635  flimfnfcls  22636  ptcmplem1  22660  clssubg  22717  tgpconncomp  22721  qustgplem  22729  tsmsfbas  22736  utoptop  22843  iducn  22892  cstucnd  22893  isxmetd  22936  isxmet2d  22937  xmettpos  22959  prdsdsf  22977  prdsmet  22980  ressprdsds  22981  imasdsf1olem  22983  imasf1oxmet  22985  imasf1omet  22986  blfvalps  22993  xmetresbl  23047  metss2  23122  comet  23123  stdbdmet  23126  stdbdmopn  23128  methaus  23130  met2ndci  23132  metustfbas  23167  nrmmetd  23184  subgngp  23244  ngptgp  23245  sranlm  23293  nlmvscnlem1  23295  nlmvscn  23296  nrginvrcn  23301  lssnlm  23310  nghmcn  23354  qtopbaslem  23367  reconn  23436  xmetdcn2  23445  metdscn  23464  metnrm  23470  elcncf1di  23503  cncffvrn  23506  mulc1cncf  23513  cncfco  23515  reparphti  23601  isncvsngpd  23754  tcphcph  23840  ipcnlem1  23848  ipcn  23849  iscfil3  23876  bcthlem5  23931  rrxmet  24011  minveclem3  24032  minveclem7  24038  ovolicc2lem4  24121  dyadmbl  24201  volcn  24207  itg1addlem1  24293  itg1addlem2  24298  itg1addlem4  24300  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  dvmptfsum  24572  c1liplem1  24593  dvgt0lem2  24600  ftc1a  24634  ply1domn  24717  ply1divmo  24729  fta1b  24763  ig1peu  24765  coeeu  24815  plydivalg  24888  aaliou2b  24930  ulmss  24985  ulmcn  24987  efif1olem4  25129  efsubm  25135  logccv  25246  logbmpt  25366  logbfval  25368  cvxcl  25562  basellem4  25661  fsumdvdscom  25762  musum  25768  dvdsmulf1o  25771  fsumdvdsmul  25772  dchrelbasd  25815  dchrmulcl  25825  dchrinv  25837  lgsqrlem2  25923  lgsdchr  25931  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  2sqreulem4  26030  dchrisumlema  26064  dchrisumlem2  26066  chpdifbndlem2  26130  pntpbnd  26164  pntibndlem3  26168  axtgcont  26255  tgjustc1  26261  tgjustc2  26262  iscgrglt  26300  ercgrg  26303  idmot  26323  motco  26326  cnvmot  26327  motcgrg  26330  tgisline  26413  tghilberti2  26424  mirreu3  26440  mirmot  26461  ragperp  26503  foot  26508  mideu  26524  midf  26562  lmimot  26584  trgcopyeu  26592  f1otrgds  26655  f1otrg  26657  f1otrge  26658  xmstrkgc  26672  brbtwn2  26691  axlowdimlem15  26742  axcontlem2  26751  axcontlem10  26759  eengtrkg  26772  eengtrkge  26773  numedglnl  26929  usgredgreu  27000  uspgredg2vtxeu  27002  uspgredg2v  27006  usgredg2v  27009  wlkswwlksf1o  27657  wwlksnextinj  27677  clwlkclwwlkf1  27788  clwwlkf1  27828  frcond4  28049  frgrncvvdeqlem8  28085  frgrncvvdeq  28088  frgrwopreglem4  28094  numclwwlk1lem2f1  28136  grpoinvf  28309  nvmf  28422  vacn  28471  nmcvcn  28472  smcnlem  28474  sspg  28505  ssps  28507  sspmlem  28509  0lno  28567  blocni  28582  ipblnfi  28632  minvecolem7  28660  unopf1o  29693  cnvunop  29695  unoplin  29697  counop  29698  hmopadj2  29718  hmoplin  29719  bralnfn  29725  lnopeq0i  29784  hmops  29797  hmopm  29798  hmopco  29800  lnconi  29810  cnlnadjlem2  29845  adjmul  29869  adjadd  29870  cdjreui  30209  disjxpin  30338  off2  30388  fnpreimac  30416  suppovss  30426  f1od2  30457  xrofsup  30492  s3f1  30623  ccatf1  30625  swrdf1  30630  odutos  30650  abliso  30683  symgcntz  30729  tocyccntz  30786  archiabllem1  30822  archiabllem2  30826  suborng  30888  xrge0slmod  30917  prmidl2  30958  isprmidlc  30963  qsidomlem1  30965  qsidomlem2  30966  mxidlprm  30977  ssmxidllem  30978  lindsun  31021  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  1smat1  31069  submateq  31074  madjusmdetlem3  31094  pstmxmet  31137  ofcf  31362  ldgenpisys  31425  rossros  31439  inelcarsg  31569  sibfof  31598  sitmf  31610  hgt750lemb  31927  erdszelem4  32441  erdszelem9  32446  erdsze2lem2  32451  cnpconn  32477  pconnconn  32478  txpconn  32479  ptpconn  32480  cvxpconn  32489  cvxsconn  32490  iccllysconn  32497  cvmseu  32523  cvmliftmo  32531  cvmlift2lem5  32554  cvmlift2lem9  32558  mrsubff1  32761  elmrsubrn  32767  mrsubco  32768  msubff1  32803  mvhf1  32806  sslttr  33268  segconeu  33472  fnessref  33705  neibastop1  33707  filnetlem3  33728  onsuct0  33789  unblimceq0lem  33845  unbdqndv2  33850  knoppndv  33873  uncf  34886  fin2so  34894  lindsadd  34900  poimirlem4  34911  poimirlem13  34920  poimirlem14  34921  poimirlem26  34933  heicant  34942  mblfinlem2  34945  ftc1anc  34990  sdclem1  35033  isbnd3  35077  prdsbnd  35086  ismtycnv  35095  ismtyhmeolem  35097  ismtyres  35101  bfplem1  35115  bfplem2  35116  bfp  35117  rrnmet  35122  ismrer1  35131  iccbnd  35133  grpokerinj  35186  isdrngo2  35251  rngogrphom  35264  rngohomco  35267  rngoisocnv  35274  iscringd  35291  erprt  36024  lfl0f  36220  lkrlss  36246  lshpsmreu  36260  linepsubN  36903  pmapsub  36919  lautcnv  37241  lautco  37248  idltrn  37301  cdleme50f1  37694  cdleme50laut  37698  istendod  37913  dihf11  38418  dih1dimatlem  38480  lcfl7N  38652  lcfrlem9  38701  mapd1o  38799  hdmapf1oN  39016  hgmapf1oN  39054  qsalrel  39145  nacsfix  39329  rmxypairf1o  39528  wepwsolem  39662  dnnumch3  39667  fnwe2  39673  mpaaeu  39770  idomsubgmo  39818  mon1psubm  39826  deg1mhm  39827  isotone1  40418  isotone2  40419  disjxp1  41351  disjf1  41463  wessf1ornlem  41465  projf1o  41479  sumnnodd  41931  lptioo2  41932  lptioo1  41933  cncfshift  42177  cncfperiod  42182  dvnprodlem1  42251  fourierdlem42  42454  nnfoctbdjlem  42757  isomennd  42833  smflimlem6  43072  otiunsndisjX  43498  imasetpreimafvbijlemf1  43584  iccpartgt  43607  icceuelpart  43616  ichnreuop  43654  sprsymrelfolem2  43675  sprsymrelf  43677  prproropf1o  43689  reupr  43704  reuopreuprim  43708  isomuspgrlem2c  44015  isomuspgr  44019  ismgmd  44063  mgmhmpropd  44072  mgmhmf1o  44074  idmgmhm  44075  issubmgm2  44077  rabsubmgmd  44078  resmgmhm  44085  resmgmhm2  44086  resmgmhm2b  44087  mgmhmco  44088  submgmacs  44091  opmpoismgm  44094  mgmplusgiopALT  44121  isrnghm2d  44192  c0mgm  44200  c0mhm  44201  lidlmmgm  44216  2zlidl  44225  rnghmsscmap2  44264  rnghmsscmap  44265  rnghmsubcsetclem2  44267  rhmsscmap2  44310  rhmsscmap  44311  rhmsubcsetclem2  44313  rhmsscrnghm  44317  rhmsubcrngclem2  44319  srhmsubc  44367  fldhmsubc  44375  rhmsubc  44381  srhmsubcALTV  44385  fldhmsubcALTV  44393  rhmsubcALTV  44399  lindslinindsimp1  44532