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 2145  ∀wral 3076

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 1943

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

This theorem is used by:  disjord  5091  disjxiun  5099  otsndisj  5488  otiunsndisj  5489  swopo  5566  issod  5590  reuop  6285  fcof1  7283  fliftfund  7309  isof1oidb  7320  isof1oopb  7321  soisores  7323  soisoi  7324  isocnv  7326  f1oiso  7347  oveqrspc2v  7435  oprres  7576  caovclg  7601  caovcomg  7604  off  7694  coof  7700  caofidlcan  7714  caofrss  7715  caonncan  7720  fmpodg  8066  dmmpog  8070  fnmpoovd  8081  fmpoco  8089  fsplitfpar  8112  poxp  8123  fvmpocurryd  8266  smo11  8350  smoiso2  8355  onelfvnef1  8427  omsmo  8645  nnasmo  8650  coflton  8658  qsdisj2  8794  eroprf  8814  uncf  8869  dom2lem  8997  omxpenlem  9075  xpf1o  9136  unxpdomlem3  9227  fofinf1o  9299  dffi3  9401  supmo  9422  infmo  9467  inf3lem6  9612  cantnf  9672  rankxplim  9869  fseqenlem1  10074  fodomacn  10106  iunfictbso  10164  cofsmo  10318  infpssrlem5  10356  enfin2i  10370  fin23lem23  10375  fin23lem27  10377  fin23lem28  10389  compssiso  10423  ltordlem  11810  cju  12285  axdc4uzlem  14094  seqcaopr2  14149  seqhomo  14160  ccatf1  14703  swrdf1  14766  wrd2ind  14839  cshf1  14928  s3sndisj  15087  s3iunsndisj  15088  climcn2  15727  addcn2  15728  mulcn2  15730  o1of2  15747  isercolllem1  15799  fsum2dlem  15903  fsumcom2  15907  fprodser  16083  fprod2dlem  16114  fprodcom2  16118  isprm6  16852  crth  16916  eulerthlem2  16920  vdwlem12  17131  cshwsdisj  17237  imasaddfnlem  17661  imasvscafn  17670  mreexexd  17783  iscatd  17808  oppccomfpropd  17862  isofn  17911  sectmon  17918  ssctr  17961  ssceq  17962  catsubcat  17975  issubc3  17985  fullsubc  17986  fullresc  17987  isfuncd  18001  idfucl  18017  cofucl  18024  funcres2b  18033  fulloppc  18060  fthoppc  18061  idffth  18071  cofull  18072  cofth  18073  ressffth  18076  setcmon  18223  setcepi  18224  resssetc  18228  resscatc  18245  catciso  18247  fthestrcsetc  18285  fullestrcsetc  18286  embedsetcestrclem  18292  fthsetcestrc  18300  fullsetcestrc  18301  evlfcl  18357  uncfcurf  18374  hofcl  18394  yonedalem3  18415  yonedainv  18416  yonffthlem  18417  yoniso  18420  isdrs2  18441  isposd  18457  pospropd  18460  poslubmo  18544  posglbmo  18545  chnpof1  18765  mgmplusf  18787  mgmn0plusgf  18788  ismgmd  18791  issstrmgm  18792  opifismgm  18798  mgmhmpropd  18848  mgmhmf1o  18850  idmgmhm  18851  issubmgm2  18853  rabsubmgmd  18854  resmgmhm  18861  resmgmhm2  18862  resmgmhm2b  18863  mgmhmco  18864  submgmacs  18867  issgrpd  18880  sgrppropd  18881  ismndd  18907  mndpropd  18912  issubmnd  18914  mndinvmod  18919  ismhmd  18942  mhmpropd  18948  idmhm  18951  mhmf1o  18952  issubmd  18962  mndissubm  18963  0mhm  18976  resmhm  18977  resmhm2  18978  resmhm2b  18979  mhmco  18980  submacs  18984  prdspjmhm  18986  pwsdiagmhm  18988  pwsco1mhm  18989  pwsco2mhm  18990  gsumwspan  19003  frmdsssubm  19018  frmdup1  19021  grpsubf  19190  dfgrp3  19210  mhmmnd  19235  mhmfmhm  19236  issubg4  19317  grpissubg  19318  isnsg3  19331  nsgacs  19333  0nsg  19340  nsgid  19341  qus0subgadd  19375  cycsubmcom  19380  isghmd  19400  ghmmhm  19401  idghm  19406  ghmnsgima  19415  ghmnsgpreima  19416  ghmf1  19421  kerf1ghm  19422  ghmf1o  19423  gaid  19474  subgga  19475  gass  19476  gasubg  19477  cntzsgrpcl  19509  cntzsubm  19513  cntrsubgnsg  19518  lactghmga  19580  symgfixf1  19612  odf1  19737  sylow1lem2  19774  sylow2blem2  19796  sylow3lem1  19802  lsmssv  19818  smndlsmidm  19831  pj1eu  19871  efglem  19891  efgtf  19897  efgred  19923  efgredeu  19927  frgpmhm  19940  frgpuptf  19945  frgpuplem  19947  mulgmhm  20002  ghmcmn  20006  invghm  20008  ablnsg  20022  imasabl  20051  cygabl  20066  gsum2d2lem  20148  gsum2d2  20149  gsumcom2  20150  dprd2d2  20221  ablfaclem2  20263  srgfcl  20383  srgcom4lem  20400  srglmhm  20408  srgrmhm  20409  ringcomlem  20469  isrnghm2d  20641  c0mgm  20650  c0mhm  20651  isrhm2d  20682  subrngringnsg  20766  issubrng2  20771  subrngint  20773  issubrg2  20805  subrgint  20808  rnghmsscmap2  20842  rnghmsscmap  20843  rnghmsubcsetclem2  20845  rhmsscmap2  20871  rhmsscmap  20872  rhmsubcsetclem2  20874  rhmsscrnghm  20878  rhmsubcrngclem2  20880  srhmsubc  20893  rhmsubc  20902  fldhmsubc  21003  primefld  21023  abvn0b  21054  suborng  21094  islmodd  21102  lmodscaf  21120  lmodprop2d  21160  islssd  21171  islss4  21198  lssacs  21203  lsspropd  21253  islmhmd  21275  lmhmima  21283  lmhmpreima  21284  reslmhm  21288  lspextmo  21292  lsmcl  21319  pj1lmhm  21336  islbs2  21393  issubrgd  21425  dflidl2rng  21458  rnglidlmmgm  21494  rhmpreimaidl  21532  rngqiprnglin  21559  prmidl2  21583  idlmulssprm  21584  isprmidlc  21589  rhmpreimaprmidl  21596  qsidomlem1  21597  qsidomlem2  21598  ssdifidllem  21601  ssdifidlprm  21603  prmidlsubm  21604  expmhm  21703  nn0srg  21704  prmirredlem  21739  expghm  21742  mulgghm2  21743  domnchr  21799  znf1o  21818  zntoslem  21823  znfld  21827  cygznlem3  21836  phlipf  21919  dsmmlss  22011  uvcf1  22059  frlmlbs  22064  lindff1  22087  lindfrn  22088  f1lindf  22089  issubassa2  22161  mvrf1  22254  mplsubglem  22267  mplsubrg  22273  mplcoe5lem  22309  mplcoe2  22311  mplind  22340  evlslem2  22349  evlseu  22353  mhplss  22437  ply1sclf1  22569  evls1maplmhm  22656  mamucl  22677  mamuass  22678  mamudi  22679  mamudir  22680  mamuvs1  22681  mamuvs2  22682  matbas2d  22699  mamumat1cl  22715  mamulid  22717  mamurid  22718  mat1mhm  22760  dmatid  22771  dmatsubcl  22774  dmatsgrp  22775  dmatmulcl  22776  dmatsrng  22777  dmatcrng  22778  scmatscmiddistr  22784  scmatscm  22789  scmatsgrp  22795  scmatsrng  22796  scmatcrng  22797  scmatsgrp1  22798  scmatsrng1  22799  scmatf1  22807  scmatmhm  22810  mavmul0g  22829  mdet1  22877  mdetunilem9  22896  mdetuni0  22897  mdetmul  22899  madutpos  22918  smadiadetlem4  22945  1elcpmat  22994  cpmatacl  22995  cpmatmcl  22998  mat2pmatf1  23008  mat2pmatmul  23010  mat2pmat1  23011  mat2pmatlin  23014  m2cpm  23020  m2cpminvid  23032  m2cpminvid2  23034  decpmatmul  23051  pmatcollpw1  23055  monmatcollpw  23058  pmatcollpw  23060  pmatcollpw3lem  23062  pmatcollpwscmatlem2  23069  pm2mpf1  23078  mp2pm2mplem4  23088  pm2mpmhmlem2  23098  chp0mat  23125  chpidmat  23126  tgclb  23249  mretopd  23371  toponmre  23372  iscldtop  23374  ordtbaslem  23467  ordtbas2  23470  cnt0  23625  haust1  23631  cnhaus  23633  isreg2  23656  dishaus  23661  ordthaus  23663  dfconn2  23698  iunconn  23707  clsconn  23709  2ndcomap  23738  dis2ndc  23740  llynlly  23757  restnlly  23762  restlly  23763  islly2  23764  llyidm  23768  nllyidm  23769  hausllycmp  23774  kgentopon  23818  txbas  23847  ptbasin2  23858  ptbasfi  23861  txcnp  23900  txcnmpt  23904  pthaus  23918  tx1stc  23930  xkococnlem  23939  xkococn  23940  cnmpt21  23951  qtoptop2  23979  qtopeu  23996  kqt0lem  24016  isr0  24017  regr1lem2  24020  kqreglem1  24021  kqreglem2  24022  kqnrmlem1  24023  kqnrmlem2  24024  nrmr0reg  24029  reghmph  24073  nrmhmph  24074  txswaphmeo  24085  qtophmeo  24097  fbun  24120  trfbas2  24123  isfil2  24136  infil  24143  trfil2  24167  filssufilg  24191  hausflim  24261  fclsnei  24299  fclsfnflim  24307  flimfnfcls  24308  ptcmplem1  24332  clssubg  24389  tgpconncomp  24393  qustgplem  24401  tsmsfbas  24408  utoptop  24514  iducn  24562  cstucnd  24563  isxmetd  24606  isxmet2d  24607  xmettpos  24629  prdsdsf  24647  prdsmet  24650  ressprdsds  24651  imasdsf1olem  24653  imasf1oxmet  24655  imasf1omet  24656  blfvalps  24663  xmetresbl  24717  metss2  24792  comet  24793  stdbdmet  24796  stdbdmopn  24798  methaus  24800  met2ndci  24802  metustfbas  24837  nrmmetd  24854  subgngp  24915  ngptgp  24916  sranlm  24964  nlmvscnlem1  24966  nlmvscn  24967  nrginvrcn  24972  lssnlm  24981  nghmcn  25025  qtopbaslem  25038  reconn  25109  xmetdcn2  25118  metdscn  25137  metnrm  25143  elcncf1di  25177  cncfcdm  25180  mulc1cncf  25187  cncfco  25189  reparphti  25279  isncvsngpd  25432  tcphcph  25519  ipcnlem1  25527  ipcn  25528  iscfil3  25555  bcthlem5  25610  rrxmet  25690  minveclem3  25711  minveclem7  25717  ovolicc2lem4  25802  dyadmbl  25882  volcn  25888  itg1addlem1  25974  itg1addlem2  25979  itg1addlem4  25981  mbfi1fseqlem1  25997  mbfi1fseqlem3  25999  mbfi1fseqlem4  26000  mbfi1fseqlem5  26001  dvmptfsum  26256  c1liplem1  26277  dvgt0lem2  26284  ftc1a  26318  ply1domn  26403  ply1divmo  26415  fta1b  26451  ig1peu  26454  coeeu  26505  plydivalg  26583  aaliou2b  26631  ulmss  26687  ulmcn  26689  efif1olem4  26836  efsubm  26842  logccv  26954  logbmpt  27079  logbfval  27081  cvxcl  27275  basellem4  27374  fsumdvdscom  27475  musum  27481  mpodvdsmulf1o  27484  fsumdvdsmul  27485  dvdsmulf1o  27486  dchrelbasd  27529  dchrmulcl  27539  dchrinv  27551  lgsqrlem2  27637  lgsdchr  27645  lgseisenlem2  27666  lgsquadlem1  27670  lgsquadlem2  27671  2sqreulem4  27744  dchrisumlema  27778  dchrisumlem2  27780  chpdifbndlem2  27844  pntpbnd  27878  pntibndlem3  27882  sltsd  28087  oldbday  28220  addsprop  28295  mulcutlem  28450  divsmo  28503  om2noseqf1o  28620  om2noseqiso  28621  axtgcont  28864  tgjustc1  28870  tgjustc2  28871  tgsegconeu  28882  iscgrglt  28910  ercgrg  28913  idmot  28933  motco  28936  cnvmot  28937  motcgrg  28940  tgisline  29028  tghilberti2  29039  mirreu3  29059  mirmot  29080  ragperp  29125  foot  29130  mideu  29147  midf  29214  lmimot  29236  trgcopyeu  29246  prlngmolem1  29363  f1otrgds  29379  f1otrg  29381  f1otrge  29382  xmstrkgc  29396  brbtwn2  29416  axlowdimlem15  29467  axcontlem2  29476  axcontlem10  29484  eengtrkg  29497  eengtrkge  29498  numedglnl  29655  usgredgreu  29732  uspgredg2vtxeu  29734  uspgredg2v  29738  usgredg2v  29741  wlkswwlksf1o  30401  wwlksnextinj  30421  clwlkclwwlkf1  30534  clwwlkf1  30573  frcond4  30804  frgrncvvdeqlem8  30840  frgrncvvdeq  30843  frgrwopreglem4  30849  numclwwlk1lem2f1  30891  nrt2irr  31007  grpoinvf  31067  nvmf  31180  vacn  31229  nmcvcn  31230  smcnlem  31232  sspg  31263  ssps  31265  sspmlem  31267  0lno  31325  blocni  31340  ipblnfi  31390  minvecolem7  31418  unopf1o  32451  cnvunop  32453  unoplin  32455  counop  32456  hmopadj2  32476  hmoplin  32477  bralnfn  32483  lnopeq0i  32542  hmops  32555  hmopm  32556  hmopco  32558  lnconi  32568  cnlnadjlem2  32603  adjmul  32627  adjadd  32628  cdjreui  32967  disjxpin  33115  off2  33168  2ndresdju  33176  fnpreimac  33197  suppovss  33207  f1od2  33244  xrofsup  33292  s3f1  33444  odutos  33462  dfmgc2lem  33489  dfmgc2  33490  pwrssmgc  33494  mgcf1o  33497  mndlactf1  33520  mndractf1  33522  abliso  33529  symgcntz  33579  tocyccntz  33638  conjga  33664  fxpsubrg  33668  archiabllem1  33687  archiabllem2  33691  urpropd  33724  elrgspnlem2  33737  rlocf1  33768  rrgsubm  33778  subrdom  33779  ricdomn1  33783  xrge0slmod  33842  nsgmgc  33896  intlidl  33903  idlinsubrg  33914  rhmimaidl  33915  mxidlprm  33928  mxidlirredi  33929  ssmxidllem  33931  drnglring  33957  dflringlem2  33960  rsprprmprmidl  33987  rsprprmprmidlb  33988  rprmirred  33996  rprmirredb  33997  1arithufdlem4  34012  selvply1rhmlema  34083  selvply1rhmlem1  34085  mplidomlem  34092  extvfvcl  34101  mplvrpmga  34110  ply1degltdimlem  34187  ply1degltdim  34188  lindsun  34190  fedgmullem1  34194  fedgmullem2  34195  fedgmul  34196  lactlmhm  34199  assalactf1o  34200  minplyirred  34276  constrsdrg  34340  1smat1  34369  submateq  34374  madjusmdetlem3  34394  zart0  34444  pstmxmet  34462  ofcf  34668  ldgenpisys  34732  rossros  34746  inelcarsg  34877  sibfof  34906  sitmf  34918  hgt750lemb  35219  erdszelem4  35880  erdszelem9  35885  erdsze2lem2  35890  cnpconn  35916  pconnconn  35917  txpconn  35918  ptpconn  35919  cvxpconn  35928  cvxsconn  35929  iccllysconn  35936  cvmseu  35962  cvmliftmo  35970  cvmlift2lem5  35993  cvmlift2lem9  35997  mrsubff1  36200  elmrsubrn  36206  mrsubco  36207  msubff1  36242  mvhf1  36245  r1peuqusdeg1  36329  segconeu  36698  nmulprop  36861  nadddilem4  36894  fnessref  37067  neibastop1  37069  filnetlem3  37090  onsuct0  37151  weiunlem  37173  unblimceq0lem  37294  unbdqndv2  37299  knoppndv  37322  irrdiff  38167  fin2so  38450  lindsadd  38456  poimirlem4  38462  poimirlem13  38471  poimirlem14  38472  poimirlem26  38484  heicant  38493  mblfinlem2  38496  ftc1anc  38539  sdclem1  38597  isbnd3  38638  prdsbnd  38647  ismtycnv  38656  ismtyhmeolem  38658  ismtyres  38662  bfplem1  38676  bfplem2  38677  bfp  38678  rrnmet  38683  ismrer1  38692  iccbnd  38694  grpokerinj  38747  isdrngo2  38812  rngogrphom  38825  rngohomco  38828  rngoisocnv  38835  iscringd  38852  eqvreldisj1  39779  erprt  39850  lfl0f  40046  lkrlss  40072  lshpsmreu  40086  linepsubN  40729  pmapsub  40745  lautcnv  41067  lautco  41074  idltrn  41127  cdleme50f1  41520  cdleme50laut  41524  istendod  41739  dihf11  42244  dih1dimatlem  42306  lcfl7N  42478  lcfrlem9  42527  mapd1o  42625  hdmapf1oN  42842  hgmapf1oN  42880  fmpocos  43207  qsalrel  43212  rediveud  43422  imacrhmcl  43506  evlselv  43539  fsuppind  43540  nacsfix  43661  rmxypairf1o  43856  wepwsolem  43987  dnnumch3  43992  fnwe2  43998  mpaaeu  44095  idomsubgmo  44138  mon1psubm  44144  deg1mhm  44145  isotone1  44992  isotone2  44993  mnringmulrcld  45170  traxext  45904  disjxp1  46007  disjf1  46119  wessf1ornlem  46121  projf1o  46132  sumnnodd  46564  lptioo2  46565  lptioo1  46566  cncfshift  46806  cncfperiod  46811  dvnprodlem1  46878  fourierdlem42  47081  nnfoctbdjlem  47387  isomennd  47463  smflimlem6  47708  fsetsnf1  48044  cfsetsnfsetf1  48051  otiunsndisjX  48271  imasetpreimafvbijlemf1  48408  iccpartgt  48431  icceuelpart  48440  ichnreuop  48476  sprsymrelfolem2  48497  sprsymrelf  48499  prproropf1o  48511  reupr  48526  reuopreuprim  48530  uhgrimprop  48912  isuspgrim0lem  48913  upgrimtrls  48926  gpgprismgr4cycllem11  49125  opmpoismgm  49186  mgmplusgiopALT  49213  2zlidl  49259  rhmsubcALTV  49304  srhmsubcALTV  49344  fldhmsubcALTV  49352  lindslinindsimp1  49491  1arymaptf1  49676  2arymaptf1  49687  eqfnovd  49898  toslat  50012  catprsc  50043  catprsc2  50044  oppcendc  50048  invfn  50060  iinfssclem2  50085  iinfssc  50087  iinfsubc  50088  discsubc  50094  nelsubclem  50097  resccatlem  50103  funchomf  50127  imasubclem2  50135  imaidfu  50140  imasubc  50181  imassc  50183  imasubc3  50186  fthcomf  50187  idfth  50188  cofidfth  50192  upeu2  50202  isnatd  50253  swapfffth  50313  diag1f1  50337  diag2f1  50339  fucoppc  50440  isthincd  50466  isthincd2  50467  oppcthinco  50469  oppcthinendcALT  50471  functhinclem4  50477  functhincfun  50479  thincfth  50482  thincciso  50483  thinccisod  50484  functermc  50538  arweuthinc  50559  arweutermc  50560  diagffth  50568  funcsn  50571  0fucterm  50573  veronesematrowd  50903  veroquadmodzerod  50906