Theorem ralrimivva 3178

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

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

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 3051

This theorem is referenced by:  disjord  5086  disjxiun  5094  otsndisj  5466  otiunsndisj  5467  swopo  5542  issod  5566  reuop  6250  fcof1  7233  fliftfund  7259  isof1oidb  7270  isof1oopb  7271  soisores  7273  soisoi  7274  isocnv  7276  f1oiso  7297  oveqrspc2v  7385  oprres  7526  caovclg  7550  caovcomg  7553  off  7640  coof  7646  caofidlcan  7660  caofrss  7661  caonncan  7666  dmmpog  8018  fnmpoovd  8029  fmpoco  8037  fsplitfpar  8060  poxp  8070  fvmpocurryd  8213  smo11  8296  smoiso2  8301  omsmo  8586  nnasmo  8591  coflton  8599  qsdisj2  8734  eroprf  8754  dom2lem  8931  omxpenlem  9008  xpf1o  9069  unxpdomlem3  9160  fofinf1o  9234  dffi3  9336  supmo  9357  infmo  9402  inf3lem6  9544  cantnf  9604  rankxplim  9793  fseqenlem1  9936  fodomacn  9968  iunfictbso  10026  cofsmo  10181  infpssrlem5  10219  enfin2i  10233  fin23lem23  10238  fin23lem27  10240  fin23lem28  10252  compssiso  10286  ltordlem  11664  cju  12143  axdc4uzlem  13908  seqcaopr2  13963  seqhomo  13974  wrd2ind  14648  cshf1  14735  s3sndisj  14892  s3iunsndisj  14893  climcn2  15518  addcn2  15519  mulcn2  15521  o1of2  15538  isercolllem1  15590  fsum2dlem  15695  fsumcom2  15699  fprodser  15874  fprod2dlem  15905  fprodcom2  15909  isprm6  16643  crth  16707  eulerthlem2  16711  vdwlem12  16922  cshwsdisj  17028  imasaddfnlem  17451  imasvscafn  17460  mreexexd  17573  iscatd  17598  oppccomfpropd  17652  isofn  17701  sectmon  17708  ssctr  17751  ssceq  17752  catsubcat  17765  issubc3  17775  fullsubc  17776  fullresc  17777  isfuncd  17791  idfucl  17807  cofucl  17814  funcres2b  17823  fulloppc  17850  fthoppc  17851  idffth  17861  cofull  17862  cofth  17863  ressffth  17866  setcmon  18013  setcepi  18014  resssetc  18018  resscatc  18035  catciso  18037  fthestrcsetc  18075  fullestrcsetc  18076  embedsetcestrclem  18082  fthsetcestrc  18090  fullsetcestrc  18091  evlfcl  18147  uncfcurf  18164  hofcl  18184  yonedalem3  18205  yonedainv  18206  yonffthlem  18207  yoniso  18210  isdrs2  18231  isposd  18247  pospropd  18250  poslubmo  18334  posglbmo  18335  chnpof1  18555  mgmplusf  18577  ismgmd  18579  issstrmgm  18580  opifismgm  18586  mgmhmpropd  18625  mgmhmf1o  18627  idmgmhm  18628  issubmgm2  18630  rabsubmgmd  18631  resmgmhm  18638  resmgmhm2  18639  resmgmhm2b  18640  mgmhmco  18641  submgmacs  18644  issgrpd  18657  sgrppropd  18658  ismndd  18683  mndpropd  18686  issubmnd  18688  mndinvmod  18691  ismhmd  18713  mhmpropd  18719  idmhm  18722  mhmf1o  18723  issubmd  18733  mndissubm  18734  0mhm  18746  resmhm  18747  resmhm2  18748  resmhm2b  18749  mhmco  18750  submacs  18754  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  gsumwspan  18773  frmdsssubm  18788  frmdup1  18791  grpsubf  18951  dfgrp3  18971  mhmmnd  18996  mhmfmhm  18997  issubg4  19077  grpissubg  19078  isnsg3  19091  nsgacs  19093  0nsg  19100  nsgid  19101  qus0subgadd  19130  cycsubmcom  19135  isghmd  19156  ghmmhm  19157  idghm  19162  ghmnsgima  19171  ghmnsgpreima  19172  ghmf1  19177  kerf1ghm  19178  ghmf1o  19179  gaid  19230  subgga  19231  gass  19232  gasubg  19233  cntzsgrpcl  19265  cntzsubm  19269  cntrsubgnsg  19274  lactghmga  19336  symgfixf1  19368  odf1  19493  sylow1lem2  19530  sylow2blem2  19552  sylow3lem1  19558  lsmssv  19574  smndlsmidm  19587  pj1eu  19627  efglem  19647  efgtf  19653  efgred  19679  efgredeu  19683  frgpmhm  19696  frgpuptf  19701  frgpuplem  19703  mulgmhm  19758  ghmcmn  19762  invghm  19764  ablnsg  19778  imasabl  19807  cygabl  19822  gsum2d2lem  19904  gsum2d2  19905  gsumcom2  19906  dprd2d2  19977  ablfaclem2  20019  srgfcl  20133  srgcom4lem  20150  srglmhm  20158  srgrmhm  20159  ringcomlem  20216  isrnghm2d  20388  c0mgm  20397  c0mhm  20398  isrhm2d  20424  subrngringnsg  20488  issubrng2  20493  subrngint  20495  issubrg2  20527  subrgint  20530  rnghmsscmap2  20564  rnghmsscmap  20565  rnghmsubcsetclem2  20567  rhmsscmap2  20593  rhmsscmap  20594  rhmsubcsetclem2  20596  rhmsscrnghm  20600  rhmsubcrngclem2  20602  srhmsubc  20615  rhmsubc  20624  fldhmsubc  20720  primefld  20740  abvn0b  20771  suborng  20811  islmodd  20819  lmodscaf  20837  lmodprop2d  20877  islssd  20888  islss4  20915  lssacs  20920  lsspropd  20971  islmhmd  20993  lmhmima  21001  lmhmpreima  21002  reslmhm  21006  lspextmo  21010  lsmcl  21037  pj1lmhm  21054  islbs2  21111  issubrgd  21143  dflidl2rng  21175  rnglidlmmgm  21202  rhmpreimaidl  21234  rngqiprnglin  21259  expmhm  21393  nn0srg  21394  prmirredlem  21429  expghm  21432  mulgghm2  21433  domnchr  21489  znf1o  21508  zntoslem  21513  znfld  21517  cygznlem3  21526  phlipf  21609  dsmmlss  21701  uvcf1  21749  frlmlbs  21754  lindff1  21777  lindfrn  21778  f1lindf  21779  issubassa2  21850  mvrf1  21943  mplsubglem  21956  mplsubrg  21962  mplcoe5lem  21996  mplcoe2  21998  mplind  22027  evlslem2  22036  evlseu  22040  mhplss  22100  ply1sclf1  22233  evls1maplmhm  22323  mamucl  22347  mamuass  22348  mamudi  22349  mamudir  22350  mamuvs1  22351  mamuvs2  22352  matbas2d  22369  mamumat1cl  22385  mamulid  22387  mamurid  22388  mat1mhm  22430  dmatid  22441  dmatsubcl  22444  dmatsgrp  22445  dmatmulcl  22446  dmatsrng  22447  dmatcrng  22448  scmatscmiddistr  22454  scmatscm  22459  scmatsgrp  22465  scmatsrng  22466  scmatcrng  22467  scmatsgrp1  22468  scmatsrng1  22469  scmatf1  22477  scmatmhm  22480  mavmul0g  22499  mdet1  22547  mdetunilem9  22566  mdetuni0  22567  mdetmul  22569  madutpos  22588  smadiadetlem4  22615  1elcpmat  22661  cpmatacl  22662  cpmatmcl  22665  mat2pmatf1  22675  mat2pmatmul  22677  mat2pmat1  22678  mat2pmatlin  22681  m2cpm  22687  m2cpminvid  22699  m2cpminvid2  22701  decpmatmul  22718  pmatcollpw1  22722  monmatcollpw  22725  pmatcollpw  22727  pmatcollpw3lem  22729  pmatcollpwscmatlem2  22736  pm2mpf1  22745  mp2pm2mplem4  22755  pm2mpmhmlem2  22765  chp0mat  22792  chpidmat  22793  tgclb  22916  mretopd  23038  toponmre  23039  iscldtop  23041  ordtbaslem  23134  ordtbas2  23137  cnt0  23292  haust1  23298  cnhaus  23300  isreg2  23323  dishaus  23328  ordthaus  23330  dfconn2  23365  iunconn  23374  clsconn  23376  2ndcomap  23404  dis2ndc  23406  llynlly  23423  restnlly  23428  restlly  23429  islly2  23430  llyidm  23434  nllyidm  23435  hausllycmp  23440  kgentopon  23484  txbas  23513  ptbasin2  23524  ptbasfi  23527  txcnp  23566  txcnmpt  23570  pthaus  23584  tx1stc  23596  xkococnlem  23605  xkococn  23606  cnmpt21  23617  qtoptop2  23645  qtopeu  23662  kqt0lem  23682  isr0  23683  regr1lem2  23686  kqreglem1  23687  kqreglem2  23688  kqnrmlem1  23689  kqnrmlem2  23690  nrmr0reg  23695  reghmph  23739  nrmhmph  23740  txswaphmeo  23751  qtophmeo  23763  fbun  23786  trfbas2  23789  isfil2  23802  infil  23809  trfil2  23833  filssufilg  23857  hausflim  23927  fclsnei  23965  fclsfnflim  23973  flimfnfcls  23974  ptcmplem1  23998  clssubg  24055  tgpconncomp  24059  qustgplem  24067  tsmsfbas  24074  utoptop  24180  iducn  24228  cstucnd  24229  isxmetd  24272  isxmet2d  24273  xmettpos  24295  prdsdsf  24313  prdsmet  24316  ressprdsds  24317  imasdsf1olem  24319  imasf1oxmet  24321  imasf1omet  24322  blfvalps  24329  xmetresbl  24383  metss2  24458  comet  24459  stdbdmet  24462  stdbdmopn  24464  methaus  24466  met2ndci  24468  metustfbas  24503  nrmmetd  24520  subgngp  24581  ngptgp  24582  sranlm  24630  nlmvscnlem1  24632  nlmvscn  24633  nrginvrcn  24638  lssnlm  24647  nghmcn  24691  qtopbaslem  24704  reconn  24775  xmetdcn2  24784  metdscn  24803  metnrm  24809  elcncf1di  24846  cncfcdm  24849  mulc1cncf  24856  cncfco  24858  reparphti  24954  reparphtiOLD  24955  isncvsngpd  25108  tcphcph  25195  ipcnlem1  25203  ipcn  25204  iscfil3  25231  bcthlem5  25286  rrxmet  25366  minveclem3  25387  minveclem7  25393  ovolicc2lem4  25479  dyadmbl  25559  volcn  25565  itg1addlem1  25651  itg1addlem2  25656  itg1addlem4  25658  mbfi1fseqlem1  25674  mbfi1fseqlem3  25676  mbfi1fseqlem4  25677  mbfi1fseqlem5  25678  dvmptfsum  25937  c1liplem1  25959  dvgt0lem2  25966  ftc1a  26002  ply1domn  26087  ply1divmo  26099  fta1b  26135  ig1peu  26138  coeeu  26188  plydivalg  26265  aaliou2b  26307  ulmss  26364  ulmcn  26366  efif1olem4  26512  efsubm  26518  logccv  26630  logbmpt  26756  logbfval  26758  cvxcl  26953  basellem4  27052  fsumdvdscom  27153  musum  27159  mpodvdsmulf1o  27162  fsumdvdsmul  27163  dvdsmulf1o  27164  fsumdvdsmulOLD  27165  dchrelbasd  27208  dchrmulcl  27218  dchrinv  27230  lgsqrlem2  27316  lgsdchr  27324  lgseisenlem2  27345  lgsquadlem1  27349  lgsquadlem2  27350  2sqreulem4  27423  dchrisumlema  27457  dchrisumlem2  27459  chpdifbndlem2  27523  pntpbnd  27557  pntibndlem3  27561  ssltd  27766  oldbday  27881  addsprop  27956  mulscutlem  28111  divsmo  28164  om2noseqf1o  28280  om2noseqiso  28281  axtgcont  28522  tgjustc1  28528  tgjustc2  28529  iscgrglt  28567  ercgrg  28570  idmot  28590  motco  28593  cnvmot  28594  motcgrg  28597  tgisline  28680  tghilberti2  28691  mirreu3  28707  mirmot  28728  ragperp  28770  foot  28775  mideu  28791  midf  28829  lmimot  28851  trgcopyeu  28859  f1otrgds  28922  f1otrg  28924  f1otrge  28925  xmstrkgc  28939  brbtwn2  28959  axlowdimlem15  29010  axcontlem2  29019  axcontlem10  29027  eengtrkg  29040  eengtrkge  29041  numedglnl  29198  usgredgreu  29272  uspgredg2vtxeu  29274  uspgredg2v  29278  usgredg2v  29281  wlkswwlksf1o  29933  wwlksnextinj  29953  clwlkclwwlkf1  30066  clwwlkf1  30105  frcond4  30326  frgrncvvdeqlem8  30362  frgrncvvdeq  30365  frgrwopreglem4  30371  numclwwlk1lem2f1  30413  nrt2irr  30529  grpoinvf  30588  nvmf  30701  vacn  30750  nmcvcn  30751  smcnlem  30753  sspg  30784  ssps  30786  sspmlem  30788  0lno  30846  blocni  30861  ipblnfi  30911  minvecolem7  30939  unopf1o  31972  cnvunop  31974  unoplin  31976  counop  31977  hmopadj2  31997  hmoplin  31998  bralnfn  32004  lnopeq0i  32063  hmops  32076  hmopm  32077  hmopco  32079  lnconi  32089  cnlnadjlem2  32124  adjmul  32148  adjadd  32149  cdjreui  32488  disjxpin  32643  off2  32699  2ndresdju  32707  fnpreimac  32728  suppovss  32739  f1od2  32777  xrofsup  32826  s3f1  33008  ccatf1  33010  swrdf1  33017  odutos  33029  dfmgc2lem  33056  dfmgc2  33057  pwrssmgc  33061  mgcf1o  33064  mndlactf1  33087  mndractf1  33089  abliso  33097  symgcntz  33146  tocyccntz  33205  conjga  33231  fxpsubrg  33235  archiabllem1  33254  archiabllem2  33258  urpropd  33292  elrgspnlem2  33304  rlocf1  33334  rrgsubm  33345  subrdom  33346  xrge0slmod  33408  nsgmgc  33472  intlidl  33480  idlinsubrg  33491  rhmimaidl  33492  prmidl2  33501  idlmulssprm  33502  isprmidlc  33507  rhmpreimaprmidl  33511  qsidomlem1  33512  qsidomlem2  33513  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  ssmxidllem  33533  rsprprmprmidl  33582  rsprprmprmidlb  33583  rprmirred  33591  rprmirredb  33592  1arithufdlem4  33607  extvfvcl  33680  mplvrpmga  33689  ply1degltdimlem  33758  ply1degltdim  33759  lindsun  33761  fedgmullem1  33765  fedgmullem2  33766  fedgmul  33767  lactlmhm  33770  assalactf1o  33771  minplyirred  33847  constrsdrg  33911  1smat1  33940  submateq  33945  madjusmdetlem3  33965  zart0  34015  pstmxmet  34033  ofcf  34239  ldgenpisys  34302  rossros  34316  inelcarsg  34447  sibfof  34476  sitmf  34488  hgt750lemb  34792  erdszelem4  35367  erdszelem9  35372  erdsze2lem2  35377  cnpconn  35403  pconnconn  35404  txpconn  35405  ptpconn  35406  cvxpconn  35415  cvxsconn  35416  iccllysconn  35423  cvmseu  35449  cvmliftmo  35457  cvmlift2lem5  35480  cvmlift2lem9  35484  mrsubff1  35687  elmrsubrn  35693  mrsubco  35694  msubff1  35729  mvhf1  35732  r1peuqusdeg1  35816  segconeu  36184  fnessref  36530  neibastop1  36532  filnetlem3  36553  onsuct0  36614  weiunlem2  36636  unblimceq0lem  36679  unbdqndv2  36684  knoppndv  36707  irrdiff  37500  uncf  37769  fin2so  37777  lindsadd  37783  poimirlem4  37794  poimirlem13  37803  poimirlem14  37804  poimirlem26  37816  heicant  37825  mblfinlem2  37828  ftc1anc  37871  sdclem1  37913  isbnd3  37954  prdsbnd  37963  ismtycnv  37972  ismtyhmeolem  37974  ismtyres  37978  bfplem1  37992  bfplem2  37993  bfp  37994  rrnmet  37999  ismrer1  38008  iccbnd  38010  grpokerinj  38063  isdrngo2  38128  rngogrphom  38141  rngohomco  38144  rngoisocnv  38151  iscringd  38168  eqvreldisj1  39097  erprt  39168  lfl0f  39364  lkrlss  39390  lshpsmreu  39404  linepsubN  40047  pmapsub  40063  lautcnv  40385  lautco  40392  idltrn  40445  cdleme50f1  40838  cdleme50laut  40842  istendod  41057  dihf11  41562  dih1dimatlem  41624  lcfl7N  41796  lcfrlem9  41845  mapd1o  41943  hdmapf1oN  42160  hgmapf1oN  42198  fmpocos  42528  qsalrel  42533  rediveud  42735  imacrhmcl  42806  evlselv  42867  fsuppind  42870  nacsfix  42991  rmxypairf1o  43190  wepwsolem  43321  dnnumch3  43326  fnwe2  43332  mpaaeu  43429  idomsubgmo  43472  mon1psubm  43478  deg1mhm  43479  isotone1  44326  isotone2  44327  mnringmulrcld  44506  traxext  45255  disjxp1  45351  disjf1  45464  wessf1ornlem  45466  projf1o  45478  sumnnodd  45913  lptioo2  45914  lptioo1  45915  cncfshift  46155  cncfperiod  46160  dvnprodlem1  46227  fourierdlem42  46430  nnfoctbdjlem  46736  isomennd  46812  smflimlem6  47057  fsetsnf1  47335  cfsetsnfsetf1  47342  otiunsndisjX  47562  imasetpreimafvbijlemf1  47687  iccpartgt  47710  icceuelpart  47719  ichnreuop  47755  sprsymrelfolem2  47776  sprsymrelf  47778  prproropf1o  47790  reupr  47805  reuopreuprim  47809  uhgrimprop  48175  isuspgrim0lem  48176  upgrimtrls  48189  gpgprismgr4cycllem11  48388  opmpoismgm  48450  mgmplusgiopALT  48477  2zlidl  48523  rhmsubcALTV  48568  srhmsubcALTV  48608  fldhmsubcALTV  48616  lindslinindsimp1  48740  1arymaptf1  48925  2arymaptf1  48936  eqfnovd  49148  fmpodg  49151  toslat  49264  catprsc  49295  catprsc2  49296  oppcendc  49300  invfn  49312  iinfssclem2  49337  iinfssc  49339  iinfsubc  49340  discsubc  49346  nelsubclem  49349  resccatlem  49355  funchomf  49379  imasubclem2  49387  imaidfu  49392  imasubc  49433  imassc  49435  imasubc3  49438  fthcomf  49439  idfth  49440  cofidfth  49444  upeu2  49454  isnatd  49505  swapfffth  49565  diag1f1  49589  diag2f1  49591  fucoppc  49692  isthincd  49718  isthincd2  49719  oppcthinco  49721  oppcthinendcALT  49723  functhinclem4  49729  functhincfun  49731  thincfth  49734  thincciso  49735  thinccisod  49736  functermc  49790  arweuthinc  49811  arweutermc  49812  diagffth  49820  funcsn  49823  0fucterm  49825