Theorem ralrimivva 3209

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

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

This theorem is used by:  disjord  5095  disjxiun  5103  otsndisj  5496  otiunsndisj  5497  swopo  5574  issod  5598  reuop  6311  fcof1  7315  fliftfund  7341  isof1oidb  7352  isof1oopb  7353  soisores  7355  soisoi  7356  isocnv  7358  f1oiso  7379  oveqrspc2v  7467  oprres  7609  caovclg  7634  caovcomg  7637  off  7732  coof  7738  caofidlcan  7752  caofrss  7753  caonncan  7758  fmpodg  8105  dmmpog  8109  fnmpoovd  8120  fmpoco  8129  f1od2  8132  fsplitfpar  8153  poxp  8164  fnwe2  8173  fvmpocurryd  8313  smo11  8397  smoiso2  8402  onelfvnef1  8474  omsmo  8692  nnasmo  8697  coflton  8705  qsdisj2  8841  eroprf  8861  uncf  8916  dom2lem  9044  omxpenlem  9122  xpf1o  9183  unxpdomlem3  9274  fofinf1o  9346  dffi3  9447  supmo  9468  infmo  9513  inf3lem6  9658  cantnf  9718  rankxplim  9920  fseqenlem1  10127  fodomacn  10159  iunfictbso  10217  cofsmo  10371  infpssrlem5  10409  enfin2i  10423  fin23lem23  10428  fin23lem27  10430  fin23lem28  10442  compssiso  10476  ltordlem  11865  cju  12340  axdc4uzlem  14150  seqcaopr2  14205  seqhomo  14216  ccatf1  14760  swrdf1  14824  wrd2ind  14897  cshf1  14986  s3sndisj  15146  s3iunsndisj  15147  climcn2  15786  addcn2  15787  mulcn2  15789  o1of2  15806  isercolllem1  15858  fsum2dlem  15962  fsumcom2  15966  fprodser  16142  fprod2dlem  16173  fprodcom2  16177  isprm6  16916  crth  16981  eulerthlem2  16985  vdwlem12  17196  cshwsdisj  17302  imasaddfnlem  17726  imasvscafn  17735  mreexexd  17848  iscatd  17873  oppccomfpropd  17927  isofn  17976  sectmon  17983  ssctr  18026  ssceq  18027  catsubcat  18040  issubc3  18050  fullsubc  18051  fullresc  18052  isfuncd  18066  idfucl  18082  cofucl  18089  funcres2b  18098  fulloppc  18125  fthoppc  18126  idffth  18136  cofull  18137  cofth  18138  ressffth  18141  setcmon  18288  setcepi  18289  resssetc  18293  resscatc  18310  catciso  18312  fthestrcsetc  18350  fullestrcsetc  18351  embedsetcestrclem  18357  fthsetcestrc  18365  fullsetcestrc  18366  evlfcl  18422  uncfcurf  18439  hofcl  18459  yonedalem3  18480  yonedainv  18481  yonffthlem  18482  yoniso  18485  isdrs2  18506  isposd  18522  pospropd  18525  poslubmo  18609  posglbmo  18610  chnpof1  18830  mgmplusf  18852  mgmn0plusgf  18853  ismgmd  18856  issstrmgm  18857  opifismgm  18863  mgmhmpropd  18913  mgmhmf1o  18915  idmgmhm  18916  issubmgm2  18918  rabsubmgmd  18919  resmgmhm  18926  resmgmhm2  18927  resmgmhm2b  18928  mgmhmco  18929  submgmacs  18932  issgrpd  18945  sgrppropd  18946  ismndd  18972  mndpropd  18977  issubmnd  18979  mndinvmod  18984  ismhmd  19007  mhmpropd  19013  idmhm  19016  mhmf1o  19017  issubmd  19027  mndissubm  19028  0mhm  19041  resmhm  19042  resmhm2  19043  resmhm2b  19044  mhmco  19045  submacs  19049  prdspjmhm  19051  pwsdiagmhm  19053  pwsco1mhm  19054  pwsco2mhm  19055  gsumwspan  19068  frmdsssubm  19083  frmdup1  19086  grpsubf  19255  dfgrp3  19275  mhmmnd  19300  mhmfmhm  19301  issubg4  19382  grpissubg  19383  isnsg3  19396  nsgacs  19398  0nsg  19405  nsgid  19406  qus0subgadd  19440  cycsubmcom  19445  isghmd  19465  ghmmhm  19466  idghm  19471  ghmnsgima  19480  ghmnsgpreima  19481  ghmf1  19486  kerf1ghm  19487  ghmf1o  19488  gaid  19540  subgga  19541  gass  19542  gasubg  19543  cntzsgrpcl  19575  cntzsubm  19579  cntrsubgnsg  19584  lactghmga  19646  symgfixf1  19678  odf1  19803  sylow1lem2  19840  sylow2blem2  19862  sylow3lem1  19868  lsmssv  19884  smndlsmidm  19897  pj1eu  19937  efglem  19957  efgtf  19963  efgred  19989  efgredeu  19993  frgpmhm  20006  frgpuptf  20011  frgpuplem  20013  mulgmhm  20068  ghmcmn  20072  invghm  20074  ablnsg  20088  imasabl  20117  cygabl  20132  gsum2d2lem  20214  gsum2d2  20215  gsumcom2  20216  dprd2d2  20287  ablfaclem2  20329  srgfcl  20449  srgcom4lem  20466  srglmhm  20474  srgrmhm  20475  ringcomlem  20535  isrnghm2d  20707  c0mgm  20716  c0mhm  20717  isrhm2d  20748  subrngringnsg  20832  issubrng2  20837  subrngint  20839  issubrg2  20871  subrgint  20874  rnghmsscmap2  20908  rnghmsscmap  20909  rnghmsubcsetclem2  20911  rhmsscmap2  20937  rhmsscmap  20938  rhmsubcsetclem2  20940  rhmsscrnghm  20944  rhmsubcrngclem2  20946  srhmsubc  20959  rhmsubc  20968  fldhmsubc  21069  primefld  21089  abvn0b  21120  suborng  21160  islmodd  21168  lmodscaf  21186  lmodprop2d  21226  islssd  21237  islss4  21264  lssacs  21269  lsspropd  21319  islmhmd  21341  lmhmima  21349  lmhmpreima  21350  reslmhm  21354  lspextmo  21358  lsmcl  21385  pj1lmhm  21402  islbs2  21459  issubrgd  21491  dflidl2rng  21524  rnglidlmmgm  21560  rhmpreimaidl  21598  rngqiprnglin  21625  prmidl2  21649  idlmulssprm  21650  isprmidlc  21655  rhmpreimaprmidl  21662  qsidomlem1  21663  qsidomlem2  21664  ssdifidllem  21667  ssdifidlprm  21669  prmidlsubm  21670  expmhm  21769  nn0srg  21770  prmirredlem  21805  expghm  21808  mulgghm2  21809  domnchr  21865  znf1o  21884  zntoslem  21889  znfld  21893  cygznlem3  21902  phlipf  21985  dsmmlss  22077  uvcf1  22125  frlmlbs  22130  lindff1  22153  lindfrn  22154  f1lindf  22155  issubassa2  22227  mvrf1  22320  mplsubglem  22333  mplsubrg  22339  mplcoe5lem  22375  mplcoe2  22377  mplind  22406  evlslem2  22415  evlseu  22419  mhplss  22503  ply1sclf1  22635  evls1maplmhm  22722  mamucl  22743  mamuass  22744  mamudi  22745  mamudir  22746  mamuvs1  22747  mamuvs2  22748  matbas2d  22765  mamumat1cl  22781  mamulid  22783  mamurid  22784  mat1mhm  22826  dmatid  22837  dmatsubcl  22840  dmatsgrp  22841  dmatmulcl  22842  dmatsrng  22843  dmatcrng  22844  scmatscmiddistr  22850  scmatscm  22855  scmatsgrp  22861  scmatsrng  22862  scmatcrng  22863  scmatsgrp1  22864  scmatsrng1  22865  scmatf1  22873  scmatmhm  22876  mavmul0g  22895  mdet1  22943  mdetunilem9  22962  mdetuni0  22963  mdetmul  22965  madutpos  22984  smadiadetlem4  23011  1elcpmat  23060  cpmatacl  23061  cpmatmcl  23064  mat2pmatf1  23074  mat2pmatmul  23076  mat2pmat1  23077  mat2pmatlin  23080  m2cpm  23086  m2cpminvid  23098  m2cpminvid2  23100  decpmatmul  23117  pmatcollpw1  23121  monmatcollpw  23124  pmatcollpw  23126  pmatcollpw3lem  23128  pmatcollpwscmatlem2  23135  pm2mpf1  23144  mp2pm2mplem4  23154  pm2mpmhmlem2  23164  chp0mat  23191  chpidmat  23192  tgclb  23315  mretopd  23437  toponmre  23438  iscldtop  23440  ordtbaslem  23533  ordtbas2  23536  cnt0  23691  haust1  23697  cnhaus  23699  isreg2  23722  dishaus  23727  ordthaus  23729  dfconn2  23764  iunconn  23773  clsconn  23775  2ndcomap  23804  dis2ndc  23806  llynlly  23823  restnlly  23828  restlly  23829  islly2  23830  llyidm  23834  nllyidm  23835  hausllycmp  23840  kgentopon  23884  txbas  23913  ptbasin2  23924  ptbasfi  23927  txcnp  23966  txcnmpt  23970  pthaus  23984  tx1stc  23996  xkococnlem  24005  xkococn  24006  cnmpt21  24017  qtoptop2  24045  qtopeu  24062  kqt0lem  24082  isr0  24083  regr1lem2  24086  kqreglem1  24087  kqreglem2  24088  kqnrmlem1  24089  kqnrmlem2  24090  nrmr0reg  24095  reghmph  24139  nrmhmph  24140  txswaphmeo  24151  qtophmeo  24163  fbun  24186  trfbas2  24189  isfil2  24202  infil  24209  trfil2  24233  filssufilg  24257  hausflim  24327  fclsnei  24365  fclsfnflim  24373  flimfnfcls  24374  ptcmplem1  24398  clssubg  24455  tgpconncomp  24459  qustgplem  24467  tsmsfbas  24474  utoptop  24580  iducn  24628  cstucnd  24629  isxmetd  24672  isxmet2d  24673  xmettpos  24695  prdsdsf  24713  prdsmet  24716  ressprdsds  24717  imasdsf1olem  24719  imasf1oxmet  24721  imasf1omet  24722  blfvalps  24729  xmetresbl  24783  metss2  24858  comet  24859  stdbdmet  24862  stdbdmopn  24864  methaus  24866  met2ndci  24868  metustfbas  24903  nrmmetd  24920  subgngp  24981  ngptgp  24982  sranlm  25030  nlmvscnlem1  25032  nlmvscn  25033  nrginvrcn  25038  lssnlm  25047  nghmcn  25091  qtopbaslem  25104  reconn  25175  xmetdcn2  25184  metdscn  25203  metnrm  25209  elcncf1di  25243  cncfcdm  25246  mulc1cncf  25253  cncfco  25255  reparphti  25345  isncvsngpd  25498  tcphcph  25585  ipcnlem1  25593  ipcn  25594  iscfil3  25621  bcthlem5  25676  rrxmet  25756  minveclem3  25777  minveclem7  25783  ovolicc2lem4  25868  dyadmbl  25948  volcn  25954  itg1addlem1  26040  itg1addlem2  26045  itg1addlem4  26047  mbfi1fseqlem1  26063  mbfi1fseqlem3  26065  mbfi1fseqlem4  26066  mbfi1fseqlem5  26067  dvmptfsum  26322  c1liplem1  26343  dvgt0lem2  26350  ftc1a  26384  ply1domn  26469  ply1divmo  26481  fta1b  26517  ig1peu  26520  coeeu  26571  plydivalg  26647  aaliou2b  26695  ulmss  26751  ulmcn  26753  efif1olem4  26900  efsubm  26906  logccv  27018  logbmpt  27143  logbfval  27145  cvxcl  27339  basellem4  27438  fsumdvdscom  27539  musum  27545  mpodvdsmulf1o  27548  fsumdvdsmul  27549  dvdsmulf1o  27550  dchrelbasd  27593  dchrmulcl  27603  dchrinv  27615  lgsqrlem2  27701  lgsdchr  27709  lgseisenlem2  27730  lgsquadlem1  27734  lgsquadlem2  27735  2sqreulem4  27808  dchrisumlema  27842  dchrisumlem2  27844  chpdifbndlem2  27908  pntpbnd  27942  pntibndlem3  27946  sltsd  28181  oldbday  28314  addsprop  28389  mulcutlem  28544  divsmo  28597  om2noseqf1o  28714  om2noseqiso  28715  axtgcont  28958  tgjustc1  28964  tgjustc2  28965  tgsegconeu  28976  iscgrglt  29004  ercgrg  29007  idmot  29027  motco  29030  cnvmot  29031  motcgrg  29034  tgisline  29122  tghilberti2  29133  mirreu3  29153  mirmot  29174  ragperp  29219  foot  29224  mideu  29241  midf  29308  lmimot  29330  trgcopyeu  29340  prlngmolem1  29457  f1otrgds  29473  f1otrg  29475  f1otrge  29476  xmstrkgc  29490  brbtwn2  29510  axlowdimlem15  29561  axcontlem2  29570  axcontlem10  29578  eengtrkg  29591  eengtrkge  29592  numedglnl  29749  usgredgreu  29826  uspgredg2vtxeu  29828  uspgredg2v  29832  usgredg2v  29835  wlkswwlksf1o  30495  wwlksnextinj  30515  clwlkclwwlkf1  30628  clwwlkf1  30667  frcond4  30898  frgrncvvdeqlem8  30934  frgrncvvdeq  30937  frgrwopreglem4  30943  numclwwlk1lem2f1  30985  nrt2irr  31101  grpoinvf  31161  nvmf  31274  vacn  31323  nmcvcn  31324  smcnlem  31326  sspg  31357  ssps  31359  sspmlem  31361  0lno  31419  blocni  31434  ipblnfi  31484  minvecolem7  31512  unopf1o  32545  cnvunop  32547  unoplin  32549  counop  32550  hmopadj2  32570  hmoplin  32571  bralnfn  32577  lnopeq0i  32636  hmops  32649  hmopm  32650  hmopco  32652  lnconi  32662  cnlnadjlem2  32697  adjmul  32721  adjadd  32722  cdjreui  33061  disjxpin  33251  off2  33304  2ndresdju  33312  fnpreimac  33333  suppovss  33342  xrofsup  33426  s3f1  33578  odutos  33596  dfmgc2lem  33623  dfmgc2  33624  pwrssmgc  33628  mgcf1o  33631  mndlactf1  33654  mndractf1  33656  abliso  33663  symgcntz  33713  tocyccntz  33772  conjga  33798  fxpsubrg  33802  archiabllem1  33821  archiabllem2  33825  urpropd  33858  elrgspnlem2  33871  rlocf1  33902  rrgsubm  33912  subrdom  33913  ricdomn1  33917  xrge0slmod  33976  nsgmgc  34030  intlidl  34037  idlinsubrg  34048  rhmimaidl  34049  mxidlprm  34062  mxidlirredi  34063  ssmxidllem  34065  drnglring  34091  dflringlem2  34094  rsprprmprmidl  34121  rsprprmprmidlb  34122  rprmirred  34130  rprmirredb  34131  1arithufdlem4  34146  selvply1rhmlema  34217  selvply1rhmlem1  34219  mplidomlem  34226  extvfvcl  34235  mplvrpmga  34244  ply1degltdimlem  34321  ply1degltdim  34322  lindsun  34324  fedgmullem1  34328  fedgmullem2  34329  fedgmul  34330  lactlmhm  34333  assalactf1o  34334  minplyirred  34410  constrsdrg  34474  1smat1  34503  submateq  34508  madjusmdetlem3  34528  zart0  34578  pstmxmet  34596  ofcf  34802  ldgenpisys  34866  rossros  34880  inelcarsg  35010  sibfof  35039  sitmf  35051  hgt750lemb  35352  j0ltalephlem  36006  erdszelem4  36125  erdszelem9  36130  erdsze2lem2  36135  cnpconn  36161  pconnconn  36162  txpconn  36163  ptpconn  36164  cvxpconn  36173  cvxsconn  36174  iccllysconn  36181  cvmseu  36207  cvmliftmo  36215  cvmlift2lem5  36238  cvmlift2lem9  36242  mrsubff1  36445  elmrsubrn  36451  mrsubco  36452  msubff1  36487  mvhf1  36490  r1peuqusdeg1  36574  segconeu  36953  nmulprop  37116  nadddilem4  37149  fnessref  37322  neibastop1  37324  filnetlem3  37345  onsuct0  37406  weiunlem  37428  unblimceq0lem  37549  unbdqndv2  37554  knoppndv  37577  irrdiff  38438  fin2so  38721  lindsadd  38727  poimirlem4  38733  poimirlem13  38742  poimirlem14  38743  poimirlem26  38755  heicant  38764  mblfinlem2  38767  ftc1anc  38810  sdclem1  38868  isbnd3  38909  prdsbnd  38918  ismtycnv  38927  ismtyhmeolem  38929  ismtyres  38933  bfplem1  38947  bfplem2  38948  bfp  38949  rrnmet  38954  ismrer1  38963  iccbnd  38965  grpokerinj  39018  isdrngo2  39083  rngogrphom  39096  rngohomco  39099  rngoisocnv  39106  iscringd  39123  eqvreldisj1  40050  erprt  40121  lfl0f  40317  lkrlss  40343  lshpsmreu  40357  linepsubN  41000  pmapsub  41016  lautcnv  41338  lautco  41345  idltrn  41398  cdleme50f1  41791  cdleme50laut  41795  istendod  42010  dihf11  42515  dih1dimatlem  42577  lcfl7N  42749  lcfrlem9  42798  mapd1o  42896  hdmapf1oN  43113  hgmapf1oN  43151  fmpocos  43478  qsalrel  43483  rediveud  43685  imacrhmcl  43772  evlselv  43808  fsuppind  43809  nacsfix  43914  rmxypairf1o  44109  wepwsolem  44240  dnnumch3  44245  mpaaeu  44342  idomsubgmo  44385  mon1psubm  44391  deg1mhm  44392  isotone1  45238  isotone2  45239  mnringmulrcld  45416  mpoexwd  46116  traxext  46160  disjxp1  46289  disjf1  46401  wessf1ornlem  46403  projf1o  46414  sumnnodd  46845  lptioo2  46846  lptioo1  46847  cncfshift  47087  cncfperiod  47092  dvnprodlem1  47159  fourierdlem42  47362  nnfoctbdjlem  47668  isomennd  47744  smflimlem6  47989  fsetsnf1  48325  cfsetsnfsetf1  48332  otiunsndisjX  48552  imasetpreimafvbijlemf1  48689  iccpartgt  48712  icceuelpart  48721  ichnreuop  48757  sprsymrelfolem2  48778  sprsymrelf  48780  prproropf1o  48792  reupr  48807  reuopreuprim  48811  uhgrimprop  49193  isuspgrim0lem  49194  upgrimtrls  49207  gpgprismgr4cycllem11  49406  opmpoismgm  49467  mgmplusgiopALT  49494  2zlidl  49540  rhmsubcALTV  49585  srhmsubcALTV  49625  fldhmsubcALTV  49633  lindslinindsimp1  49772  1arymaptf1  49957  2arymaptf1  49968  eqfnovd  50180  toslat  50299  catprsc  50330  catprsc2  50331  oppcendc  50335  invfn  50347  iinfssclem2  50372  iinfssc  50374  iinfsubc  50375  discsubc  50381  nelsubclem  50384  resccatlem  50390  funchomf  50416  imasubclem2  50424  imaidfu  50429  imasubc  50470  imassc  50472  imasubc3  50475  fthcomf  50476  idfth  50477  cofidfth  50481  upeu2  50491  isnatd  50542  swapfffth  50608  diag1f1  50632  diag2f1  50634  fucoppc  50748  isthincd  50774  isthincd2  50775  oppcthinco  50777  oppcthinendcALT  50779  functhinclem4  50785  functhincfun  50787  thincfth  50790  thincciso  50791  thinccisod  50792  functermc  50846  arweuthinc  50867  arweutermc  50868  diagffth  50879  funcsn  50882  0fucterm  50884  veronesematrowd  51259  veroquadmodzerod  51262