Theorem ralrimivva 3180

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 3178	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  5088  disjxiun  5096  otsndisj  5468  otiunsndisj  5469  swopo  5544  issod  5568  reuop  6252  fcof1  7235  fliftfund  7261  isof1oidb  7272  isof1oopb  7273  soisores  7275  soisoi  7276  isocnv  7278  f1oiso  7299  oveqrspc2v  7387  oprres  7528  caovclg  7552  caovcomg  7555  off  7642  coof  7648  caofidlcan  7662  caofrss  7663  caonncan  7668  dmmpog  8020  fnmpoovd  8031  fmpoco  8039  fsplitfpar  8062  poxp  8072  fvmpocurryd  8215  smo11  8298  smoiso2  8303  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  9546  cantnf  9606  rankxplim  9795  fseqenlem1  9938  fodomacn  9970  iunfictbso  10028  cofsmo  10183  infpssrlem5  10221  enfin2i  10235  fin23lem23  10240  fin23lem27  10242  fin23lem28  10254  compssiso  10288  ltordlem  11666  cju  12145  axdc4uzlem  13910  seqcaopr2  13965  seqhomo  13976  wrd2ind  14650  cshf1  14737  s3sndisj  14894  s3iunsndisj  14895  climcn2  15520  addcn2  15521  mulcn2  15523  o1of2  15540  isercolllem1  15592  fsum2dlem  15697  fsumcom2  15701  fprodser  15876  fprod2dlem  15907  fprodcom2  15911  isprm6  16645  crth  16709  eulerthlem2  16713  vdwlem12  16924  cshwsdisj  17030  imasaddfnlem  17453  imasvscafn  17462  mreexexd  17575  iscatd  17600  oppccomfpropd  17654  isofn  17703  sectmon  17710  ssctr  17753  ssceq  17754  catsubcat  17767  issubc3  17777  fullsubc  17778  fullresc  17779  isfuncd  17793  idfucl  17809  cofucl  17816  funcres2b  17825  fulloppc  17852  fthoppc  17853  idffth  17863  cofull  17864  cofth  17865  ressffth  17868  setcmon  18015  setcepi  18016  resssetc  18020  resscatc  18037  catciso  18039  fthestrcsetc  18077  fullestrcsetc  18078  embedsetcestrclem  18084  fthsetcestrc  18092  fullsetcestrc  18093  evlfcl  18149  uncfcurf  18166  hofcl  18186  yonedalem3  18207  yonedainv  18208  yonffthlem  18209  yoniso  18212  isdrs2  18233  isposd  18249  pospropd  18252  poslubmo  18336  posglbmo  18337  chnpof1  18557  mgmplusf  18579  ismgmd  18581  issstrmgm  18582  opifismgm  18588  mgmhmpropd  18627  mgmhmf1o  18629  idmgmhm  18630  issubmgm2  18632  rabsubmgmd  18633  resmgmhm  18640  resmgmhm2  18641  resmgmhm2b  18642  mgmhmco  18643  submgmacs  18646  issgrpd  18659  sgrppropd  18660  ismndd  18685  mndpropd  18688  issubmnd  18690  mndinvmod  18693  ismhmd  18715  mhmpropd  18721  idmhm  18724  mhmf1o  18725  issubmd  18735  mndissubm  18736  0mhm  18748  resmhm  18749  resmhm2  18750  resmhm2b  18751  mhmco  18752  submacs  18756  prdspjmhm  18758  pwsdiagmhm  18760  pwsco1mhm  18761  pwsco2mhm  18762  gsumwspan  18775  frmdsssubm  18790  frmdup1  18793  grpsubf  18953  dfgrp3  18973  mhmmnd  18998  mhmfmhm  18999  issubg4  19079  grpissubg  19080  isnsg3  19093  nsgacs  19095  0nsg  19102  nsgid  19103  qus0subgadd  19132  cycsubmcom  19137  isghmd  19158  ghmmhm  19159  idghm  19164  ghmnsgima  19173  ghmnsgpreima  19174  ghmf1  19179  kerf1ghm  19180  ghmf1o  19181  gaid  19232  subgga  19233  gass  19234  gasubg  19235  cntzsgrpcl  19267  cntzsubm  19271  cntrsubgnsg  19276  lactghmga  19338  symgfixf1  19370  odf1  19495  sylow1lem2  19532  sylow2blem2  19554  sylow3lem1  19560  lsmssv  19576  smndlsmidm  19589  pj1eu  19629  efglem  19649  efgtf  19655  efgred  19681  efgredeu  19685  frgpmhm  19698  frgpuptf  19703  frgpuplem  19705  mulgmhm  19760  ghmcmn  19764  invghm  19766  ablnsg  19780  imasabl  19809  cygabl  19824  gsum2d2lem  19906  gsum2d2  19907  gsumcom2  19908  dprd2d2  19979  ablfaclem2  20021  srgfcl  20135  srgcom4lem  20152  srglmhm  20160  srgrmhm  20161  ringcomlem  20218  isrnghm2d  20390  c0mgm  20399  c0mhm  20400  isrhm2d  20426  subrngringnsg  20490  issubrng2  20495  subrngint  20497  issubrg2  20529  subrgint  20532  rnghmsscmap2  20566  rnghmsscmap  20567  rnghmsubcsetclem2  20569  rhmsscmap2  20595  rhmsscmap  20596  rhmsubcsetclem2  20598  rhmsscrnghm  20602  rhmsubcrngclem2  20604  srhmsubc  20617  rhmsubc  20626  fldhmsubc  20722  primefld  20742  abvn0b  20773  suborng  20813  islmodd  20821  lmodscaf  20839  lmodprop2d  20879  islssd  20890  islss4  20917  lssacs  20922  lsspropd  20973  islmhmd  20995  lmhmima  21003  lmhmpreima  21004  reslmhm  21008  lspextmo  21012  lsmcl  21039  pj1lmhm  21056  islbs2  21113  issubrgd  21145  dflidl2rng  21177  rnglidlmmgm  21204  rhmpreimaidl  21236  rngqiprnglin  21261  expmhm  21395  nn0srg  21396  prmirredlem  21431  expghm  21434  mulgghm2  21435  domnchr  21491  znf1o  21510  zntoslem  21515  znfld  21519  cygznlem3  21528  phlipf  21611  dsmmlss  21703  uvcf1  21751  frlmlbs  21756  lindff1  21779  lindfrn  21780  f1lindf  21781  issubassa2  21852  mvrf1  21945  mplsubglem  21958  mplsubrg  21964  mplcoe5lem  21998  mplcoe2  22000  mplind  22029  evlslem2  22038  evlseu  22042  mhplss  22102  ply1sclf1  22235  evls1maplmhm  22325  mamucl  22349  mamuass  22350  mamudi  22351  mamudir  22352  mamuvs1  22353  mamuvs2  22354  matbas2d  22371  mamumat1cl  22387  mamulid  22389  mamurid  22390  mat1mhm  22432  dmatid  22443  dmatsubcl  22446  dmatsgrp  22447  dmatmulcl  22448  dmatsrng  22449  dmatcrng  22450  scmatscmiddistr  22456  scmatscm  22461  scmatsgrp  22467  scmatsrng  22468  scmatcrng  22469  scmatsgrp1  22470  scmatsrng1  22471  scmatf1  22479  scmatmhm  22482  mavmul0g  22501  mdet1  22549  mdetunilem9  22568  mdetuni0  22569  mdetmul  22571  madutpos  22590  smadiadetlem4  22617  1elcpmat  22663  cpmatacl  22664  cpmatmcl  22667  mat2pmatf1  22677  mat2pmatmul  22679  mat2pmat1  22680  mat2pmatlin  22683  m2cpm  22689  m2cpminvid  22701  m2cpminvid2  22703  decpmatmul  22720  pmatcollpw1  22724  monmatcollpw  22727  pmatcollpw  22729  pmatcollpw3lem  22731  pmatcollpwscmatlem2  22738  pm2mpf1  22747  mp2pm2mplem4  22757  pm2mpmhmlem2  22767  chp0mat  22794  chpidmat  22795  tgclb  22918  mretopd  23040  toponmre  23041  iscldtop  23043  ordtbaslem  23136  ordtbas2  23139  cnt0  23294  haust1  23300  cnhaus  23302  isreg2  23325  dishaus  23330  ordthaus  23332  dfconn2  23367  iunconn  23376  clsconn  23378  2ndcomap  23406  dis2ndc  23408  llynlly  23425  restnlly  23430  restlly  23431  islly2  23432  llyidm  23436  nllyidm  23437  hausllycmp  23442  kgentopon  23486  txbas  23515  ptbasin2  23526  ptbasfi  23529  txcnp  23568  txcnmpt  23572  pthaus  23586  tx1stc  23598  xkococnlem  23607  xkococn  23608  cnmpt21  23619  qtoptop2  23647  qtopeu  23664  kqt0lem  23684  isr0  23685  regr1lem2  23688  kqreglem1  23689  kqreglem2  23690  kqnrmlem1  23691  kqnrmlem2  23692  nrmr0reg  23697  reghmph  23741  nrmhmph  23742  txswaphmeo  23753  qtophmeo  23765  fbun  23788  trfbas2  23791  isfil2  23804  infil  23811  trfil2  23835  filssufilg  23859  hausflim  23929  fclsnei  23967  fclsfnflim  23975  flimfnfcls  23976  ptcmplem1  24000  clssubg  24057  tgpconncomp  24061  qustgplem  24069  tsmsfbas  24076  utoptop  24182  iducn  24230  cstucnd  24231  isxmetd  24274  isxmet2d  24275  xmettpos  24297  prdsdsf  24315  prdsmet  24318  ressprdsds  24319  imasdsf1olem  24321  imasf1oxmet  24323  imasf1omet  24324  blfvalps  24331  xmetresbl  24385  metss2  24460  comet  24461  stdbdmet  24464  stdbdmopn  24466  methaus  24468  met2ndci  24470  metustfbas  24505  nrmmetd  24522  subgngp  24583  ngptgp  24584  sranlm  24632  nlmvscnlem1  24634  nlmvscn  24635  nrginvrcn  24640  lssnlm  24649  nghmcn  24693  qtopbaslem  24706  reconn  24777  xmetdcn2  24786  metdscn  24805  metnrm  24811  elcncf1di  24848  cncfcdm  24851  mulc1cncf  24858  cncfco  24860  reparphti  24956  reparphtiOLD  24957  isncvsngpd  25110  tcphcph  25197  ipcnlem1  25205  ipcn  25206  iscfil3  25233  bcthlem5  25288  rrxmet  25368  minveclem3  25389  minveclem7  25395  ovolicc2lem4  25481  dyadmbl  25561  volcn  25567  itg1addlem1  25653  itg1addlem2  25658  itg1addlem4  25660  mbfi1fseqlem1  25676  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  dvmptfsum  25939  c1liplem1  25961  dvgt0lem2  25968  ftc1a  26004  ply1domn  26089  ply1divmo  26101  fta1b  26137  ig1peu  26140  coeeu  26190  plydivalg  26267  aaliou2b  26309  ulmss  26366  ulmcn  26368  efif1olem4  26514  efsubm  26520  logccv  26632  logbmpt  26758  logbfval  26760  cvxcl  26955  basellem4  27054  fsumdvdscom  27155  musum  27161  mpodvdsmulf1o  27164  fsumdvdsmul  27165  dvdsmulf1o  27166  fsumdvdsmulOLD  27167  dchrelbasd  27210  dchrmulcl  27220  dchrinv  27232  lgsqrlem2  27318  lgsdchr  27326  lgseisenlem2  27347  lgsquadlem1  27351  lgsquadlem2  27352  2sqreulem4  27425  dchrisumlema  27459  dchrisumlem2  27461  chpdifbndlem2  27525  pntpbnd  27559  pntibndlem3  27563  sltsd  27768  oldbday  27901  addsprop  27976  mulcutlem  28131  divsmo  28184  om2noseqf1o  28301  om2noseqiso  28302  axtgcont  28545  tgjustc1  28551  tgjustc2  28552  iscgrglt  28590  ercgrg  28593  idmot  28613  motco  28616  cnvmot  28617  motcgrg  28620  tgisline  28703  tghilberti2  28714  mirreu3  28730  mirmot  28751  ragperp  28793  foot  28798  mideu  28814  midf  28852  lmimot  28874  trgcopyeu  28882  f1otrgds  28945  f1otrg  28947  f1otrge  28948  xmstrkgc  28962  brbtwn2  28982  axlowdimlem15  29033  axcontlem2  29042  axcontlem10  29050  eengtrkg  29063  eengtrkge  29064  numedglnl  29221  usgredgreu  29295  uspgredg2vtxeu  29297  uspgredg2v  29301  usgredg2v  29304  wlkswwlksf1o  29956  wwlksnextinj  29976  clwlkclwwlkf1  30089  clwwlkf1  30128  frcond4  30349  frgrncvvdeqlem8  30385  frgrncvvdeq  30388  frgrwopreglem4  30394  numclwwlk1lem2f1  30436  nrt2irr  30552  grpoinvf  30611  nvmf  30724  vacn  30773  nmcvcn  30774  smcnlem  30776  sspg  30807  ssps  30809  sspmlem  30811  0lno  30869  blocni  30884  ipblnfi  30934  minvecolem7  30962  unopf1o  31995  cnvunop  31997  unoplin  31999  counop  32000  hmopadj2  32020  hmoplin  32021  bralnfn  32027  lnopeq0i  32086  hmops  32099  hmopm  32100  hmopco  32102  lnconi  32112  cnlnadjlem2  32147  adjmul  32171  adjadd  32172  cdjreui  32511  disjxpin  32666  off2  32722  2ndresdju  32730  fnpreimac  32751  suppovss  32762  f1od2  32800  xrofsup  32849  s3f1  33031  ccatf1  33033  swrdf1  33040  odutos  33052  dfmgc2lem  33079  dfmgc2  33080  pwrssmgc  33084  mgcf1o  33087  mndlactf1  33110  mndractf1  33112  abliso  33120  symgcntz  33169  tocyccntz  33228  conjga  33254  fxpsubrg  33258  archiabllem1  33277  archiabllem2  33281  urpropd  33315  elrgspnlem2  33327  rlocf1  33357  rrgsubm  33368  subrdom  33369  xrge0slmod  33431  nsgmgc  33495  intlidl  33503  idlinsubrg  33514  rhmimaidl  33515  prmidl2  33524  idlmulssprm  33525  isprmidlc  33530  rhmpreimaprmidl  33534  qsidomlem1  33535  qsidomlem2  33536  ssdifidllem  33539  ssdifidlprm  33541  mxidlprm  33553  mxidlirredi  33554  ssmxidllem  33556  rsprprmprmidl  33605  rsprprmprmidlb  33606  rprmirred  33614  rprmirredb  33615  1arithufdlem4  33630  extvfvcl  33703  mplvrpmga  33712  ply1degltdimlem  33781  ply1degltdim  33782  lindsun  33784  fedgmullem1  33788  fedgmullem2  33789  fedgmul  33790  lactlmhm  33793  assalactf1o  33794  minplyirred  33870  constrsdrg  33934  1smat1  33963  submateq  33968  madjusmdetlem3  33988  zart0  34038  pstmxmet  34056  ofcf  34262  ldgenpisys  34325  rossros  34339  inelcarsg  34470  sibfof  34499  sitmf  34511  hgt750lemb  34815  erdszelem4  35390  erdszelem9  35395  erdsze2lem2  35400  cnpconn  35426  pconnconn  35427  txpconn  35428  ptpconn  35429  cvxpconn  35438  cvxsconn  35439  iccllysconn  35446  cvmseu  35472  cvmliftmo  35480  cvmlift2lem5  35503  cvmlift2lem9  35507  mrsubff1  35710  elmrsubrn  35716  mrsubco  35717  msubff1  35752  mvhf1  35755  r1peuqusdeg1  35839  segconeu  36207  fnessref  36553  neibastop1  36555  filnetlem3  36576  onsuct0  36637  weiunlem  36659  unblimceq0lem  36708  unbdqndv2  36713  knoppndv  36736  irrdiff  37533  uncf  37802  fin2so  37810  lindsadd  37816  poimirlem4  37827  poimirlem13  37836  poimirlem14  37837  poimirlem26  37849  heicant  37858  mblfinlem2  37861  ftc1anc  37904  sdclem1  37946  isbnd3  37987  prdsbnd  37996  ismtycnv  38005  ismtyhmeolem  38007  ismtyres  38011  bfplem1  38025  bfplem2  38026  bfp  38027  rrnmet  38032  ismrer1  38041  iccbnd  38043  grpokerinj  38096  isdrngo2  38161  rngogrphom  38174  rngohomco  38177  rngoisocnv  38184  iscringd  38201  eqvreldisj1  39130  erprt  39201  lfl0f  39397  lkrlss  39423  lshpsmreu  39437  linepsubN  40080  pmapsub  40096  lautcnv  40418  lautco  40425  idltrn  40478  cdleme50f1  40871  cdleme50laut  40875  istendod  41090  dihf11  41595  dih1dimatlem  41657  lcfl7N  41829  lcfrlem9  41878  mapd1o  41976  hdmapf1oN  42193  hgmapf1oN  42231  fmpocos  42558  qsalrel  42563  rediveud  42765  imacrhmcl  42836  evlselv  42897  fsuppind  42900  nacsfix  43021  rmxypairf1o  43220  wepwsolem  43351  dnnumch3  43356  fnwe2  43362  mpaaeu  43459  idomsubgmo  43502  mon1psubm  43508  deg1mhm  43509  isotone1  44356  isotone2  44357  mnringmulrcld  44536  traxext  45285  disjxp1  45381  disjf1  45494  wessf1ornlem  45496  projf1o  45508  sumnnodd  45943  lptioo2  45944  lptioo1  45945  cncfshift  46185  cncfperiod  46190  dvnprodlem1  46257  fourierdlem42  46460  nnfoctbdjlem  46766  isomennd  46842  smflimlem6  47087  fsetsnf1  47365  cfsetsnfsetf1  47372  otiunsndisjX  47592  imasetpreimafvbijlemf1  47717  iccpartgt  47740  icceuelpart  47749  ichnreuop  47785  sprsymrelfolem2  47806  sprsymrelf  47808  prproropf1o  47820  reupr  47835  reuopreuprim  47839  uhgrimprop  48205  isuspgrim0lem  48206  upgrimtrls  48219  gpgprismgr4cycllem11  48418  opmpoismgm  48480  mgmplusgiopALT  48507  2zlidl  48553  rhmsubcALTV  48598  srhmsubcALTV  48638  fldhmsubcALTV  48646  lindslinindsimp1  48770  1arymaptf1  48955  2arymaptf1  48966  eqfnovd  49178  fmpodg  49181  toslat  49294  catprsc  49325  catprsc2  49326  oppcendc  49330  invfn  49342  iinfssclem2  49367  iinfssc  49369  iinfsubc  49370  discsubc  49376  nelsubclem  49379  resccatlem  49385  funchomf  49409  imasubclem2  49417  imaidfu  49422  imasubc  49463  imassc  49465  imasubc3  49468  fthcomf  49469  idfth  49470  cofidfth  49474  upeu2  49484  isnatd  49535  swapfffth  49595  diag1f1  49619  diag2f1  49621  fucoppc  49722  isthincd  49748  isthincd2  49749  oppcthinco  49751  oppcthinendcALT  49753  functhinclem4  49759  functhincfun  49761  thincfth  49764  thincciso  49765  thinccisod  49766  functermc  49820  arweuthinc  49841  arweutermc  49842  diagffth  49850  funcsn  49853  0fucterm  49855