Theorem ralrimivva 3184

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  disjord  5063  disjxiun  5071  otsndisj  5462  otiunsndisj  5463  swopo  5539  issod  5563  reuop  6247  fcof1  7234  fliftfund  7260  isof1oidb  7271  isof1oopb  7272  soisores  7274  soisoi  7275  isocnv  7277  f1oiso  7298  oveqrspc2v  7386  oprres  7527  caovclg  7551  caovcomg  7554  off  7641  coof  7647  caofidlcan  7661  caofrss  7662  caonncan  7667  dmmpog  8018  fnmpoovd  8028  fmpoco  8036  fsplitfpar  8059  poxp  8070  fvmpocurryd  8213  smo11  8297  smoiso2  8302  omsmo  8588  nnasmo  8593  coflton  8601  qsdisj2  8736  eroprf  8756  dom2lem  8933  omxpenlem  9010  xpf1o  9071  unxpdomlem3  9162  fofinf1o  9236  dffi3  9338  supmo  9359  infmo  9404  inf3lem6  9549  cantnf  9609  rankxplim  9798  fseqenlem1  9941  fodomacn  9973  iunfictbso  10031  cofsmo  10187  infpssrlem5  10225  enfin2i  10239  fin23lem23  10244  fin23lem27  10246  fin23lem28  10258  compssiso  10292  ltordlem  11671  cju  12150  axdc4uzlem  13940  seqcaopr2  13995  seqhomo  14006  wrd2ind  14680  cshf1  14767  s3sndisj  14924  s3iunsndisj  14925  climcn2  15550  addcn2  15551  mulcn2  15553  o1of2  15570  isercolllem1  15622  fsum2dlem  15727  fsumcom2  15731  fprodser  15909  fprod2dlem  15940  fprodcom2  15944  isprm6  16679  crth  16743  eulerthlem2  16747  vdwlem12  16958  cshwsdisj  17064  imasaddfnlem  17487  imasvscafn  17496  mreexexd  17609  iscatd  17634  oppccomfpropd  17688  isofn  17737  sectmon  17744  ssctr  17787  ssceq  17788  catsubcat  17801  issubc3  17811  fullsubc  17812  fullresc  17813  isfuncd  17827  idfucl  17843  cofucl  17850  funcres2b  17859  fulloppc  17886  fthoppc  17887  idffth  17897  cofull  17898  cofth  17899  ressffth  17902  setcmon  18049  setcepi  18050  resssetc  18054  resscatc  18071  catciso  18073  fthestrcsetc  18111  fullestrcsetc  18112  embedsetcestrclem  18118  fthsetcestrc  18126  fullsetcestrc  18127  evlfcl  18183  uncfcurf  18200  hofcl  18220  yonedalem3  18241  yonedainv  18242  yonffthlem  18243  yoniso  18246  isdrs2  18267  isposd  18283  pospropd  18286  poslubmo  18370  posglbmo  18371  chnpof1  18591  mgmplusf  18613  ismgmd  18615  issstrmgm  18616  opifismgm  18622  mgmhmpropd  18661  mgmhmf1o  18663  idmgmhm  18664  issubmgm2  18666  rabsubmgmd  18667  resmgmhm  18674  resmgmhm2  18675  resmgmhm2b  18676  mgmhmco  18677  submgmacs  18680  issgrpd  18693  sgrppropd  18694  ismndd  18719  mndpropd  18722  issubmnd  18724  mndinvmod  18727  ismhmd  18749  mhmpropd  18755  idmhm  18758  mhmf1o  18759  issubmd  18769  mndissubm  18770  0mhm  18782  resmhm  18783  resmhm2  18784  resmhm2b  18785  mhmco  18786  submacs  18790  prdspjmhm  18792  pwsdiagmhm  18794  pwsco1mhm  18795  pwsco2mhm  18796  gsumwspan  18809  frmdsssubm  18824  frmdup1  18827  grpsubf  18990  dfgrp3  19010  mhmmnd  19035  mhmfmhm  19036  issubg4  19116  grpissubg  19117  isnsg3  19130  nsgacs  19132  0nsg  19139  nsgid  19140  qus0subgadd  19169  cycsubmcom  19174  isghmd  19194  ghmmhm  19195  idghm  19200  ghmnsgima  19209  ghmnsgpreima  19210  ghmf1  19215  kerf1ghm  19216  ghmf1o  19217  gaid  19268  subgga  19269  gass  19270  gasubg  19271  cntzsgrpcl  19303  cntzsubm  19307  cntrsubgnsg  19312  lactghmga  19374  symgfixf1  19406  odf1  19531  sylow1lem2  19568  sylow2blem2  19590  sylow3lem1  19596  lsmssv  19612  smndlsmidm  19625  pj1eu  19665  efglem  19685  efgtf  19691  efgred  19717  efgredeu  19721  frgpmhm  19734  frgpuptf  19739  frgpuplem  19741  mulgmhm  19796  ghmcmn  19800  invghm  19802  ablnsg  19816  imasabl  19845  cygabl  19860  gsum2d2lem  19942  gsum2d2  19943  gsumcom2  19944  dprd2d2  20015  ablfaclem2  20057  srgfcl  20171  srgcom4lem  20188  srglmhm  20196  srgrmhm  20197  ringcomlem  20254  isrnghm2d  20424  c0mgm  20433  c0mhm  20434  isrhm2d  20461  subrngringnsg  20528  issubrng2  20533  subrngint  20535  issubrg2  20567  subrgint  20570  rnghmsscmap2  20604  rnghmsscmap  20605  rnghmsubcsetclem2  20607  rhmsscmap2  20633  rhmsscmap  20634  rhmsubcsetclem2  20636  rhmsscrnghm  20640  rhmsubcrngclem2  20642  srhmsubc  20655  rhmsubc  20664  fldhmsubc  20760  primefld  20780  abvn0b  20811  suborng  20851  islmodd  20859  lmodscaf  20877  lmodprop2d  20917  islssd  20928  islss4  20955  lssacs  20960  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  21414  nn0srg  21415  prmirredlem  21450  expghm  21453  mulgghm2  21454  domnchr  21510  znf1o  21529  zntoslem  21534  znfld  21538  cygznlem3  21547  phlipf  21630  dsmmlss  21722  uvcf1  21770  frlmlbs  21775  lindff1  21798  lindfrn  21799  f1lindf  21800  issubassa2  21870  mvrf1  21963  mplsubglem  21976  mplsubrg  21982  mplcoe5lem  22018  mplcoe2  22020  mplind  22049  evlslem2  22058  evlseu  22062  mhplss  22146  ply1sclf1  22278  evls1maplmhm  22366  mamucl  22387  mamuass  22388  mamudi  22389  mamudir  22390  mamuvs1  22391  mamuvs2  22392  matbas2d  22409  mamumat1cl  22425  mamulid  22427  mamurid  22428  mat1mhm  22470  dmatid  22481  dmatsubcl  22484  dmatsgrp  22485  dmatmulcl  22486  dmatsrng  22487  dmatcrng  22488  scmatscmiddistr  22494  scmatscm  22499  scmatsgrp  22505  scmatsrng  22506  scmatcrng  22507  scmatsgrp1  22508  scmatsrng1  22509  scmatf1  22517  scmatmhm  22520  mavmul0g  22539  mdet1  22587  mdetunilem9  22606  mdetuni0  22607  mdetmul  22609  madutpos  22628  smadiadetlem4  22655  1elcpmat  22701  cpmatacl  22702  cpmatmcl  22705  mat2pmatf1  22715  mat2pmatmul  22717  mat2pmat1  22718  mat2pmatlin  22721  m2cpm  22727  m2cpminvid  22739  m2cpminvid2  22741  decpmatmul  22758  pmatcollpw1  22762  monmatcollpw  22765  pmatcollpw  22767  pmatcollpw3lem  22769  pmatcollpwscmatlem2  22776  pm2mpf1  22785  mp2pm2mplem4  22795  pm2mpmhmlem2  22805  chp0mat  22832  chpidmat  22833  tgclb  22956  mretopd  23078  toponmre  23079  iscldtop  23081  ordtbaslem  23174  ordtbas2  23177  cnt0  23332  haust1  23338  cnhaus  23340  isreg2  23363  dishaus  23368  ordthaus  23370  dfconn2  23405  iunconn  23414  clsconn  23416  2ndcomap  23444  dis2ndc  23446  llynlly  23463  restnlly  23468  restlly  23469  islly2  23470  llyidm  23474  nllyidm  23475  hausllycmp  23480  kgentopon  23524  txbas  23553  ptbasin2  23564  ptbasfi  23567  txcnp  23606  txcnmpt  23610  pthaus  23624  tx1stc  23636  xkococnlem  23645  xkococn  23646  cnmpt21  23657  qtoptop2  23685  qtopeu  23702  kqt0lem  23722  isr0  23723  regr1lem2  23726  kqreglem1  23727  kqreglem2  23728  kqnrmlem1  23729  kqnrmlem2  23730  nrmr0reg  23735  reghmph  23779  nrmhmph  23780  txswaphmeo  23791  qtophmeo  23803  fbun  23826  trfbas2  23829  isfil2  23842  infil  23849  trfil2  23873  filssufilg  23897  hausflim  23967  fclsnei  24005  fclsfnflim  24013  flimfnfcls  24014  ptcmplem1  24038  clssubg  24095  tgpconncomp  24099  qustgplem  24107  tsmsfbas  24114  utoptop  24220  iducn  24268  cstucnd  24269  isxmetd  24312  isxmet2d  24313  xmettpos  24335  prdsdsf  24353  prdsmet  24356  ressprdsds  24357  imasdsf1olem  24359  imasf1oxmet  24361  imasf1omet  24362  blfvalps  24369  xmetresbl  24423  metss2  24498  comet  24499  stdbdmet  24502  stdbdmopn  24504  methaus  24506  met2ndci  24508  metustfbas  24543  nrmmetd  24560  subgngp  24621  ngptgp  24622  sranlm  24670  nlmvscnlem1  24672  nlmvscn  24673  nrginvrcn  24678  lssnlm  24687  nghmcn  24731  qtopbaslem  24744  reconn  24815  xmetdcn2  24824  metdscn  24843  metnrm  24849  elcncf1di  24883  cncfcdm  24886  mulc1cncf  24893  cncfco  24895  reparphti  24985  isncvsngpd  25138  tcphcph  25225  ipcnlem1  25233  ipcn  25234  iscfil3  25261  bcthlem5  25316  rrxmet  25396  minveclem3  25417  minveclem7  25423  ovolicc2lem4  25508  dyadmbl  25588  volcn  25594  itg1addlem1  25680  itg1addlem2  25685  itg1addlem4  25687  mbfi1fseqlem1  25703  mbfi1fseqlem3  25705  mbfi1fseqlem4  25706  mbfi1fseqlem5  25707  dvmptfsum  25963  c1liplem1  25984  dvgt0lem2  25991  ftc1a  26025  ply1domn  26110  ply1divmo  26122  fta1b  26158  ig1peu  26161  coeeu  26211  plydivalg  26286  aaliou2b  26328  ulmss  26383  ulmcn  26385  efif1olem4  26530  efsubm  26536  logccv  26648  logbmpt  26773  logbfval  26775  cvxcl  26969  basellem4  27068  fsumdvdscom  27169  musum  27175  mpodvdsmulf1o  27178  fsumdvdsmul  27179  dvdsmulf1o  27180  dchrelbasd  27223  dchrmulcl  27233  dchrinv  27245  lgsqrlem2  27331  lgsdchr  27339  lgseisenlem2  27360  lgsquadlem1  27364  lgsquadlem2  27365  2sqreulem4  27438  dchrisumlema  27472  dchrisumlem2  27474  chpdifbndlem2  27538  pntpbnd  27572  pntibndlem3  27576  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  29967  wwlksnextinj  29987  clwlkclwwlkf1  30100  clwwlkf1  30139  frcond4  30360  frgrncvvdeqlem8  30396  frgrncvvdeq  30399  frgrwopreglem4  30405  numclwwlk1lem2f1  30447  nrt2irr  30563  grpoinvf  30623  nvmf  30736  vacn  30785  nmcvcn  30786  smcnlem  30788  sspg  30819  ssps  30821  sspmlem  30823  0lno  30881  blocni  30896  ipblnfi  30946  minvecolem7  30974  unopf1o  32007  cnvunop  32009  unoplin  32011  counop  32012  hmopadj2  32032  hmoplin  32033  bralnfn  32039  lnopeq0i  32098  hmops  32111  hmopm  32112  hmopco  32114  lnconi  32124  cnlnadjlem2  32159  adjmul  32183  adjadd  32184  cdjreui  32523  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  33168  tocyccntz  33227  conjga  33253  fxpsubrg  33257  archiabllem1  33276  archiabllem2  33280  urpropd  33314  elrgspnlem2  33326  rlocf1  33356  rrgsubm  33367  subrdom  33368  ricdomn1  33372  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  drnglring  33585  dflringlem2  33588  rsprprmprmidl  33615  rsprprmprmidlb  33616  rprmirred  33624  rprmirredb  33625  1arithufdlem4  33640  selvply1rhmlema  33712  selvply1rhmlem1  33714  mplidomlem  33721  extvfvcl  33730  mplvrpmga  33739  ply1degltdimlem  33816  ply1degltdim  33817  lindsun  33819  fedgmullem1  33823  fedgmullem2  33824  fedgmul  33825  lactlmhm  33828  assalactf1o  33829  minplyirred  33905  constrsdrg  33969  1smat1  33998  submateq  34003  madjusmdetlem3  34023  zart0  34073  pstmxmet  34091  ofcf  34297  ldgenpisys  34360  rossros  34374  inelcarsg  34505  sibfof  34534  sitmf  34546  hgt750lemb  34850  erdszelem4  35435  erdszelem9  35440  erdsze2lem2  35445  cnpconn  35471  pconnconn  35472  txpconn  35473  ptpconn  35474  cvxpconn  35483  cvxsconn  35484  iccllysconn  35491  cvmseu  35517  cvmliftmo  35525  cvmlift2lem5  35548  cvmlift2lem9  35552  mrsubff1  35755  elmrsubrn  35761  mrsubco  35762  msubff1  35797  mvhf1  35800  r1peuqusdeg1  35884  segconeu  36252  fnessref  36598  neibastop1  36600  filnetlem3  36621  onsuct0  36682  weiunlem  36704  mh-inf3f1  36782  unblimceq0lem  36825  unbdqndv2  36830  knoppndv  36853  irrdiff  37699  uncf  37979  fin2so  37987  lindsadd  37993  poimirlem4  38004  poimirlem13  38013  poimirlem14  38014  poimirlem26  38026  heicant  38035  mblfinlem2  38038  ftc1anc  38081  sdclem1  38123  isbnd3  38164  prdsbnd  38173  ismtycnv  38182  ismtyhmeolem  38184  ismtyres  38188  bfplem1  38202  bfplem2  38203  bfp  38204  rrnmet  38209  ismrer1  38218  iccbnd  38220  grpokerinj  38273  isdrngo2  38338  rngogrphom  38351  rngohomco  38354  rngoisocnv  38361  iscringd  38378  eqvreldisj1  39307  erprt  39378  lfl0f  39574  lkrlss  39600  lshpsmreu  39614  linepsubN  40257  pmapsub  40273  lautcnv  40595  lautco  40602  idltrn  40655  cdleme50f1  41048  cdleme50laut  41052  istendod  41267  dihf11  41772  dih1dimatlem  41834  lcfl7N  42006  lcfrlem9  42055  mapd1o  42153  hdmapf1oN  42370  hgmapf1oN  42408  fmpocos  42733  qsalrel  42738  rediveud  42933  imacrhmcl  43017  evlselv  43052  fsuppind  43053  nacsfix  43174  rmxypairf1o  43369  wepwsolem  43500  dnnumch3  43505  fnwe2  43511  mpaaeu  43608  idomsubgmo  43651  mon1psubm  43657  deg1mhm  43658  isotone1  44505  isotone2  44506  mnringmulrcld  44685  traxext  45434  disjxp1  45530  disjf1  45642  wessf1ornlem  45644  projf1o  45655  sumnnodd  46087  lptioo2  46088  lptioo1  46089  cncfshift  46329  cncfperiod  46334  dvnprodlem1  46401  fourierdlem42  46604  nnfoctbdjlem  46910  isomennd  46986  smflimlem6  47231  fsetsnf1  47527  cfsetsnfsetf1  47534  otiunsndisjX  47754  imasetpreimafvbijlemf1  47891  iccpartgt  47914  icceuelpart  47923  ichnreuop  47959  sprsymrelfolem2  47980  sprsymrelf  47982  prproropf1o  47994  reupr  48009  reuopreuprim  48013  uhgrimprop  48395  isuspgrim0lem  48396  upgrimtrls  48409  gpgprismgr4cycllem11  48608  opmpoismgm  48670  mgmplusgiopALT  48697  2zlidl  48743  rhmsubcALTV  48788  srhmsubcALTV  48828  fldhmsubcALTV  48836  lindslinindsimp1  48960  1arymaptf1  49145  2arymaptf1  49156  eqfnovd  49368  fmpodg  49371  toslat  49484  catprsc  49515  catprsc2  49516  oppcendc  49520  invfn  49532  iinfssclem2  49557  iinfssc  49559  iinfsubc  49560  discsubc  49566  nelsubclem  49569  resccatlem  49575  funchomf  49599  imasubclem2  49607  imaidfu  49612  imasubc  49653  imassc  49655  imasubc3  49658  fthcomf  49659  idfth  49660  cofidfth  49664  upeu2  49674  isnatd  49725  swapfffth  49785  diag1f1  49809  diag2f1  49811  fucoppc  49912  isthincd  49938  isthincd2  49939  oppcthinco  49941  oppcthinendcALT  49943  functhinclem4  49949  functhincfun  49951  thincfth  49954  thincciso  49955  thinccisod  49956  functermc  50010  arweuthinc  50031  arweutermc  50032  diagffth  50040  funcsn  50043  0fucterm  50045