Theorem ralrimivva 3205

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  disjord  5091  disjxiun  5099  otsndisj  5491  otiunsndisj  5492  swopo  5569  issod  5593  reuop  6296  fcof1  7295  fliftfund  7321  isof1oidb  7332  isof1oopb  7333  soisores  7335  soisoi  7336  isocnv  7338  f1oiso  7359  oveqrspc2v  7447  oprres  7588  caovclg  7613  caovcomg  7616  off  7711  coof  7717  caofidlcan  7731  caofrss  7732  caonncan  7737  fmpodg  8083  dmmpog  8087  fnmpoovd  8098  fmpoco  8106  fsplitfpar  8129  poxp  8140  fnwe2  8149  fvmpocurryd  8288  smo11  8372  smoiso2  8377  onelfvnef1  8449  omsmo  8667  nnasmo  8672  coflton  8680  qsdisj2  8816  eroprf  8836  uncf  8891  dom2lem  9019  omxpenlem  9097  xpf1o  9158  unxpdomlem3  9249  fofinf1o  9321  dffi3  9423  supmo  9444  infmo  9489  inf3lem6  9634  cantnf  9694  rankxplim  9896  fseqenlem1  10103  fodomacn  10135  iunfictbso  10193  cofsmo  10347  infpssrlem5  10385  enfin2i  10399  fin23lem23  10404  fin23lem27  10406  fin23lem28  10418  compssiso  10452  ltordlem  11841  cju  12316  axdc4uzlem  14126  seqcaopr2  14181  seqhomo  14192  ccatf1  14736  swrdf1  14799  wrd2ind  14872  cshf1  14961  s3sndisj  15120  s3iunsndisj  15121  climcn2  15760  addcn2  15761  mulcn2  15763  o1of2  15780  isercolllem1  15832  fsum2dlem  15936  fsumcom2  15940  fprodser  16116  fprod2dlem  16147  fprodcom2  16151  isprm6  16890  crth  16955  eulerthlem2  16959  vdwlem12  17170  cshwsdisj  17276  imasaddfnlem  17700  imasvscafn  17709  mreexexd  17822  iscatd  17847  oppccomfpropd  17901  isofn  17950  sectmon  17957  ssctr  18000  ssceq  18001  catsubcat  18014  issubc3  18024  fullsubc  18025  fullresc  18026  isfuncd  18040  idfucl  18056  cofucl  18063  funcres2b  18072  fulloppc  18099  fthoppc  18100  idffth  18110  cofull  18111  cofth  18112  ressffth  18115  setcmon  18262  setcepi  18263  resssetc  18267  resscatc  18284  catciso  18286  fthestrcsetc  18324  fullestrcsetc  18325  embedsetcestrclem  18331  fthsetcestrc  18339  fullsetcestrc  18340  evlfcl  18396  uncfcurf  18413  hofcl  18433  yonedalem3  18454  yonedainv  18455  yonffthlem  18456  yoniso  18459  isdrs2  18480  isposd  18496  pospropd  18499  poslubmo  18583  posglbmo  18584  chnpof1  18804  mgmplusf  18826  mgmn0plusgf  18827  ismgmd  18830  issstrmgm  18831  opifismgm  18837  mgmhmpropd  18887  mgmhmf1o  18889  idmgmhm  18890  issubmgm2  18892  rabsubmgmd  18893  resmgmhm  18900  resmgmhm2  18901  resmgmhm2b  18902  mgmhmco  18903  submgmacs  18906  issgrpd  18919  sgrppropd  18920  ismndd  18946  mndpropd  18951  issubmnd  18953  mndinvmod  18958  ismhmd  18981  mhmpropd  18987  idmhm  18990  mhmf1o  18991  issubmd  19001  mndissubm  19002  0mhm  19015  resmhm  19016  resmhm2  19017  resmhm2b  19018  mhmco  19019  submacs  19023  prdspjmhm  19025  pwsdiagmhm  19027  pwsco1mhm  19028  pwsco2mhm  19029  gsumwspan  19042  frmdsssubm  19057  frmdup1  19060  grpsubf  19229  dfgrp3  19249  mhmmnd  19274  mhmfmhm  19275  issubg4  19356  grpissubg  19357  isnsg3  19370  nsgacs  19372  0nsg  19379  nsgid  19380  qus0subgadd  19414  cycsubmcom  19419  isghmd  19439  ghmmhm  19440  idghm  19445  ghmnsgima  19454  ghmnsgpreima  19455  ghmf1  19460  kerf1ghm  19461  ghmf1o  19462  gaid  19513  subgga  19514  gass  19515  gasubg  19516  cntzsgrpcl  19548  cntzsubm  19552  cntrsubgnsg  19557  lactghmga  19619  symgfixf1  19651  odf1  19776  sylow1lem2  19813  sylow2blem2  19835  sylow3lem1  19841  lsmssv  19857  smndlsmidm  19870  pj1eu  19910  efglem  19930  efgtf  19936  efgred  19962  efgredeu  19966  frgpmhm  19979  frgpuptf  19984  frgpuplem  19986  mulgmhm  20041  ghmcmn  20045  invghm  20047  ablnsg  20061  imasabl  20090  cygabl  20105  gsum2d2lem  20187  gsum2d2  20188  gsumcom2  20189  dprd2d2  20260  ablfaclem2  20302  srgfcl  20422  srgcom4lem  20439  srglmhm  20447  srgrmhm  20448  ringcomlem  20508  isrnghm2d  20680  c0mgm  20689  c0mhm  20690  isrhm2d  20721  subrngringnsg  20805  issubrng2  20810  subrngint  20812  issubrg2  20844  subrgint  20847  rnghmsscmap2  20881  rnghmsscmap  20882  rnghmsubcsetclem2  20884  rhmsscmap2  20910  rhmsscmap  20911  rhmsubcsetclem2  20913  rhmsscrnghm  20917  rhmsubcrngclem2  20919  srhmsubc  20932  rhmsubc  20941  fldhmsubc  21042  primefld  21062  abvn0b  21093  suborng  21133  islmodd  21141  lmodscaf  21159  lmodprop2d  21199  islssd  21210  islss4  21237  lssacs  21242  lsspropd  21292  islmhmd  21314  lmhmima  21322  lmhmpreima  21323  reslmhm  21327  lspextmo  21331  lsmcl  21358  pj1lmhm  21375  islbs2  21432  issubrgd  21464  dflidl2rng  21497  rnglidlmmgm  21533  rhmpreimaidl  21571  rngqiprnglin  21598  prmidl2  21622  idlmulssprm  21623  isprmidlc  21628  rhmpreimaprmidl  21635  qsidomlem1  21636  qsidomlem2  21637  ssdifidllem  21640  ssdifidlprm  21642  prmidlsubm  21643  expmhm  21742  nn0srg  21743  prmirredlem  21778  expghm  21781  mulgghm2  21782  domnchr  21838  znf1o  21857  zntoslem  21862  znfld  21866  cygznlem3  21875  phlipf  21958  dsmmlss  22050  uvcf1  22098  frlmlbs  22103  lindff1  22126  lindfrn  22127  f1lindf  22128  issubassa2  22200  mvrf1  22293  mplsubglem  22306  mplsubrg  22312  mplcoe5lem  22348  mplcoe2  22350  mplind  22379  evlslem2  22388  evlseu  22392  mhplss  22476  ply1sclf1  22608  evls1maplmhm  22695  mamucl  22716  mamuass  22717  mamudi  22718  mamudir  22719  mamuvs1  22720  mamuvs2  22721  matbas2d  22738  mamumat1cl  22754  mamulid  22756  mamurid  22757  mat1mhm  22799  dmatid  22810  dmatsubcl  22813  dmatsgrp  22814  dmatmulcl  22815  dmatsrng  22816  dmatcrng  22817  scmatscmiddistr  22823  scmatscm  22828  scmatsgrp  22834  scmatsrng  22835  scmatcrng  22836  scmatsgrp1  22837  scmatsrng1  22838  scmatf1  22846  scmatmhm  22849  mavmul0g  22868  mdet1  22916  mdetunilem9  22935  mdetuni0  22936  mdetmul  22938  madutpos  22957  smadiadetlem4  22984  1elcpmat  23033  cpmatacl  23034  cpmatmcl  23037  mat2pmatf1  23047  mat2pmatmul  23049  mat2pmat1  23050  mat2pmatlin  23053  m2cpm  23059  m2cpminvid  23071  m2cpminvid2  23073  decpmatmul  23090  pmatcollpw1  23094  monmatcollpw  23097  pmatcollpw  23099  pmatcollpw3lem  23101  pmatcollpwscmatlem2  23108  pm2mpf1  23117  mp2pm2mplem4  23127  pm2mpmhmlem2  23137  chp0mat  23164  chpidmat  23165  tgclb  23288  mretopd  23410  toponmre  23411  iscldtop  23413  ordtbaslem  23506  ordtbas2  23509  cnt0  23664  haust1  23670  cnhaus  23672  isreg2  23695  dishaus  23700  ordthaus  23702  dfconn2  23737  iunconn  23746  clsconn  23748  2ndcomap  23777  dis2ndc  23779  llynlly  23796  restnlly  23801  restlly  23802  islly2  23803  llyidm  23807  nllyidm  23808  hausllycmp  23813  kgentopon  23857  txbas  23886  ptbasin2  23897  ptbasfi  23900  txcnp  23939  txcnmpt  23943  pthaus  23957  tx1stc  23969  xkococnlem  23978  xkococn  23979  cnmpt21  23990  qtoptop2  24018  qtopeu  24035  kqt0lem  24055  isr0  24056  regr1lem2  24059  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  nrmr0reg  24068  reghmph  24112  nrmhmph  24113  txswaphmeo  24124  qtophmeo  24136  fbun  24159  trfbas2  24162  isfil2  24175  infil  24182  trfil2  24206  filssufilg  24230  hausflim  24300  fclsnei  24338  fclsfnflim  24346  flimfnfcls  24347  ptcmplem1  24371  clssubg  24428  tgpconncomp  24432  qustgplem  24440  tsmsfbas  24447  utoptop  24553  iducn  24601  cstucnd  24602  isxmetd  24645  isxmet2d  24646  xmettpos  24668  prdsdsf  24686  prdsmet  24689  ressprdsds  24690  imasdsf1olem  24692  imasf1oxmet  24694  imasf1omet  24695  blfvalps  24702  xmetresbl  24756  metss2  24831  comet  24832  stdbdmet  24835  stdbdmopn  24837  methaus  24839  met2ndci  24841  metustfbas  24876  nrmmetd  24893  subgngp  24954  ngptgp  24955  sranlm  25003  nlmvscnlem1  25005  nlmvscn  25006  nrginvrcn  25011  lssnlm  25020  nghmcn  25064  qtopbaslem  25077  reconn  25148  xmetdcn2  25157  metdscn  25176  metnrm  25182  elcncf1di  25216  cncfcdm  25219  mulc1cncf  25226  cncfco  25228  reparphti  25318  isncvsngpd  25471  tcphcph  25558  ipcnlem1  25566  ipcn  25567  iscfil3  25594  bcthlem5  25649  rrxmet  25729  minveclem3  25750  minveclem7  25756  ovolicc2lem4  25841  dyadmbl  25921  volcn  25927  itg1addlem1  26013  itg1addlem2  26018  itg1addlem4  26020  mbfi1fseqlem1  26036  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  dvmptfsum  26295  c1liplem1  26316  dvgt0lem2  26323  ftc1a  26357  ply1domn  26442  ply1divmo  26454  fta1b  26490  ig1peu  26493  coeeu  26544  plydivalg  26620  aaliou2b  26668  ulmss  26724  ulmcn  26726  efif1olem4  26873  efsubm  26879  logccv  26991  logbmpt  27116  logbfval  27118  cvxcl  27312  basellem4  27411  fsumdvdscom  27512  musum  27518  mpodvdsmulf1o  27521  fsumdvdsmul  27522  dvdsmulf1o  27523  dchrelbasd  27566  dchrmulcl  27576  dchrinv  27588  lgsqrlem2  27674  lgsdchr  27682  lgseisenlem2  27703  lgsquadlem1  27707  lgsquadlem2  27708  2sqreulem4  27781  dchrisumlema  27815  dchrisumlem2  27817  chpdifbndlem2  27881  pntpbnd  27915  pntibndlem3  27919  sltsd  28154  oldbday  28287  addsprop  28362  mulcutlem  28517  divsmo  28570  om2noseqf1o  28687  om2noseqiso  28688  axtgcont  28931  tgjustc1  28937  tgjustc2  28938  tgsegconeu  28949  iscgrglt  28977  ercgrg  28980  idmot  29000  motco  29003  cnvmot  29004  motcgrg  29007  tgisline  29095  tghilberti2  29106  mirreu3  29126  mirmot  29147  ragperp  29192  foot  29197  mideu  29214  midf  29281  lmimot  29303  trgcopyeu  29313  prlngmolem1  29430  f1otrgds  29446  f1otrg  29448  f1otrge  29449  xmstrkgc  29463  brbtwn2  29483  axlowdimlem15  29534  axcontlem2  29543  axcontlem10  29551  eengtrkg  29564  eengtrkge  29565  numedglnl  29722  usgredgreu  29799  uspgredg2vtxeu  29801  uspgredg2v  29805  usgredg2v  29808  wlkswwlksf1o  30468  wwlksnextinj  30488  clwlkclwwlkf1  30601  clwwlkf1  30640  frcond4  30871  frgrncvvdeqlem8  30907  frgrncvvdeq  30910  frgrwopreglem4  30916  numclwwlk1lem2f1  30958  nrt2irr  31074  grpoinvf  31134  nvmf  31247  vacn  31296  nmcvcn  31297  smcnlem  31299  sspg  31330  ssps  31332  sspmlem  31334  0lno  31392  blocni  31407  ipblnfi  31457  minvecolem7  31485  unopf1o  32518  cnvunop  32520  unoplin  32522  counop  32523  hmopadj2  32543  hmoplin  32544  bralnfn  32550  lnopeq0i  32609  hmops  32622  hmopm  32623  hmopco  32625  lnconi  32635  cnlnadjlem2  32670  adjmul  32694  adjadd  32695  cdjreui  33034  disjxpin  33182  off2  33235  2ndresdju  33243  fnpreimac  33264  suppovss  33274  f1od2  33311  xrofsup  33359  s3f1  33511  odutos  33529  dfmgc2lem  33556  dfmgc2  33557  pwrssmgc  33561  mgcf1o  33564  mndlactf1  33587  mndractf1  33589  abliso  33596  symgcntz  33646  tocyccntz  33705  conjga  33731  fxpsubrg  33735  archiabllem1  33754  archiabllem2  33758  urpropd  33791  elrgspnlem2  33804  rlocf1  33835  rrgsubm  33845  subrdom  33846  ricdomn1  33850  xrge0slmod  33909  nsgmgc  33963  intlidl  33970  idlinsubrg  33981  rhmimaidl  33982  mxidlprm  33995  mxidlirredi  33996  ssmxidllem  33998  drnglring  34024  dflringlem2  34027  rsprprmprmidl  34054  rsprprmprmidlb  34055  rprmirred  34063  rprmirredb  34064  1arithufdlem4  34079  selvply1rhmlema  34150  selvply1rhmlem1  34152  mplidomlem  34159  extvfvcl  34168  mplvrpmga  34177  ply1degltdimlem  34254  ply1degltdim  34255  lindsun  34257  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  lactlmhm  34266  assalactf1o  34267  minplyirred  34343  constrsdrg  34407  1smat1  34436  submateq  34441  madjusmdetlem3  34461  zart0  34511  pstmxmet  34529  ofcf  34735  ldgenpisys  34799  rossros  34813  inelcarsg  34943  sibfof  34972  sitmf  34984  hgt750lemb  35285  erdszelem4  35959  erdszelem9  35964  erdsze2lem2  35969  cnpconn  35995  pconnconn  35996  txpconn  35997  ptpconn  35998  cvxpconn  36007  cvxsconn  36008  iccllysconn  36015  cvmseu  36041  cvmliftmo  36049  cvmlift2lem5  36072  cvmlift2lem9  36076  mrsubff1  36279  elmrsubrn  36285  mrsubco  36286  msubff1  36321  mvhf1  36324  r1peuqusdeg1  36408  segconeu  36776  nmulprop  36939  nadddilem4  36972  fnessref  37145  neibastop1  37147  filnetlem3  37168  onsuct0  37229  weiunlem  37251  unblimceq0lem  37372  unbdqndv2  37377  knoppndv  37400  irrdiff  38248  fin2so  38531  lindsadd  38537  poimirlem4  38543  poimirlem13  38552  poimirlem14  38553  poimirlem26  38565  heicant  38574  mblfinlem2  38577  ftc1anc  38620  sdclem1  38678  isbnd3  38719  prdsbnd  38728  ismtycnv  38737  ismtyhmeolem  38739  ismtyres  38743  bfplem1  38757  bfplem2  38758  bfp  38759  rrnmet  38764  ismrer1  38773  iccbnd  38775  grpokerinj  38828  isdrngo2  38893  rngogrphom  38906  rngohomco  38909  rngoisocnv  38916  iscringd  38933  eqvreldisj1  39860  erprt  39931  lfl0f  40127  lkrlss  40153  lshpsmreu  40167  linepsubN  40810  pmapsub  40826  lautcnv  41148  lautco  41155  idltrn  41208  cdleme50f1  41601  cdleme50laut  41605  istendod  41820  dihf11  42325  dih1dimatlem  42387  lcfl7N  42559  lcfrlem9  42608  mapd1o  42706  hdmapf1oN  42923  hgmapf1oN  42961  fmpocos  43288  qsalrel  43293  rediveud  43495  imacrhmcl  43582  evlselv  43618  fsuppind  43619  nacsfix  43723  rmxypairf1o  43918  wepwsolem  44049  dnnumch3  44054  mpaaeu  44152  idomsubgmo  44195  mon1psubm  44201  deg1mhm  44202  isotone1  45048  isotone2  45049  mnringmulrcld  45226  traxext  45967  disjxp1  46086  disjf1  46198  wessf1ornlem  46200  projf1o  46211  sumnnodd  46642  lptioo2  46643  lptioo1  46644  cncfshift  46884  cncfperiod  46889  dvnprodlem1  46956  fourierdlem42  47159  nnfoctbdjlem  47465  isomennd  47541  smflimlem6  47786  fsetsnf1  48122  cfsetsnfsetf1  48129  otiunsndisjX  48349  imasetpreimafvbijlemf1  48486  iccpartgt  48509  icceuelpart  48518  ichnreuop  48554  sprsymrelfolem2  48575  sprsymrelf  48577  prproropf1o  48589  reupr  48604  reuopreuprim  48608  uhgrimprop  48990  isuspgrim0lem  48991  upgrimtrls  49004  gpgprismgr4cycllem11  49203  opmpoismgm  49264  mgmplusgiopALT  49291  2zlidl  49337  rhmsubcALTV  49382  srhmsubcALTV  49422  fldhmsubcALTV  49430  lindslinindsimp1  49569  1arymaptf1  49754  2arymaptf1  49765  eqfnovd  49976  toslat  50090  catprsc  50121  catprsc2  50122  oppcendc  50126  invfn  50138  iinfssclem2  50163  iinfssc  50165  iinfsubc  50166  discsubc  50172  nelsubclem  50175  resccatlem  50181  funchomf  50205  imasubclem2  50213  imaidfu  50218  imasubc  50259  imassc  50261  imasubc3  50264  fthcomf  50265  idfth  50266  cofidfth  50270  upeu2  50280  isnatd  50331  swapfffth  50391  diag1f1  50415  diag2f1  50417  fucoppc  50518  isthincd  50544  isthincd2  50545  oppcthinco  50547  oppcthinendcALT  50549  functhinclem4  50555  functhincfun  50557  thincfth  50560  thincciso  50561  thinccisod  50562  functermc  50616  arweuthinc  50637  arweutermc  50638  diagffth  50646  funcsn  50649  0fucterm  50651  veronesematrowd  50981  veroquadmodzerod  50984