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  5092  disjxiun  5100  otsndisj  5496  otiunsndisj  5497  swopo  5574  issod  5598  reuop  6291  fcof1  7289  fliftfund  7315  isof1oidb  7326  isof1oopb  7327  soisores  7329  soisoi  7330  isocnv  7332  f1oiso  7353  oveqrspc2v  7441  oprres  7582  caovclg  7607  caovcomg  7610  off  7697  coof  7703  caofidlcan  7717  caofrss  7718  caonncan  7723  fmpodg  8070  dmmpog  8074  fnmpoovd  8085  fmpoco  8093  fsplitfpar  8116  poxp  8127  fvmpocurryd  8270  smo11  8354  smoiso2  8359  omsmo  8647  nnasmo  8652  coflton  8660  qsdisj2  8796  eroprf  8816  uncf  8871  dom2lem  8999  omxpenlem  9077  xpf1o  9138  unxpdomlem3  9229  fofinf1o  9300  dffi3  9402  supmo  9423  infmo  9468  inf3lem6  9613  cantnf  9673  rankxplim  9862  fseqenlem1  10028  fodomacn  10060  iunfictbso  10118  cofsmo  10272  infpssrlem5  10310  enfin2i  10324  fin23lem23  10329  fin23lem27  10331  fin23lem28  10343  compssiso  10377  ltordlem  11764  cju  12239  axdc4uzlem  14048  seqcaopr2  14103  seqhomo  14114  ccatf1  14657  swrdf1  14720  wrd2ind  14793  cshf1  14882  s3sndisj  15041  s3iunsndisj  15042  climcn2  15681  addcn2  15682  mulcn2  15684  o1of2  15701  isercolllem1  15753  fsum2dlem  15857  fsumcom2  15861  fprodser  16037  fprod2dlem  16068  fprodcom2  16072  isprm6  16806  crth  16870  eulerthlem2  16874  vdwlem12  17085  cshwsdisj  17191  imasaddfnlem  17615  imasvscafn  17624  mreexexd  17737  iscatd  17762  oppccomfpropd  17816  isofn  17865  sectmon  17872  ssctr  17915  ssceq  17916  catsubcat  17929  issubc3  17939  fullsubc  17940  fullresc  17941  isfuncd  17955  idfucl  17971  cofucl  17978  funcres2b  17987  fulloppc  18014  fthoppc  18015  idffth  18025  cofull  18026  cofth  18027  ressffth  18030  setcmon  18177  setcepi  18178  resssetc  18182  resscatc  18199  catciso  18201  fthestrcsetc  18239  fullestrcsetc  18240  embedsetcestrclem  18246  fthsetcestrc  18254  fullsetcestrc  18255  evlfcl  18311  uncfcurf  18328  hofcl  18348  yonedalem3  18369  yonedainv  18370  yonffthlem  18371  yoniso  18374  isdrs2  18395  isposd  18411  pospropd  18414  poslubmo  18498  posglbmo  18499  chnpof1  18719  mgmplusf  18741  mgmn0plusgf  18742  ismgmd  18745  issstrmgm  18746  opifismgm  18752  mgmhmpropd  18801  mgmhmf1o  18803  idmgmhm  18804  issubmgm2  18806  rabsubmgmd  18807  resmgmhm  18814  resmgmhm2  18815  resmgmhm2b  18816  mgmhmco  18817  submgmacs  18820  issgrpd  18833  sgrppropd  18834  ismndd  18860  mndpropd  18865  issubmnd  18867  mndinvmod  18872  ismhmd  18895  mhmpropd  18901  idmhm  18904  mhmf1o  18905  issubmd  18915  mndissubm  18916  0mhm  18929  resmhm  18930  resmhm2  18931  resmhm2b  18932  mhmco  18933  submacs  18937  prdspjmhm  18939  pwsdiagmhm  18941  pwsco1mhm  18942  pwsco2mhm  18943  gsumwspan  18956  frmdsssubm  18971  frmdup1  18974  grpsubf  19143  dfgrp3  19163  mhmmnd  19188  mhmfmhm  19189  issubg4  19270  grpissubg  19271  isnsg3  19284  nsgacs  19286  0nsg  19293  nsgid  19294  qus0subgadd  19328  cycsubmcom  19333  isghmd  19353  ghmmhm  19354  idghm  19359  ghmnsgima  19368  ghmnsgpreima  19369  ghmf1  19374  kerf1ghm  19375  ghmf1o  19376  gaid  19427  subgga  19428  gass  19429  gasubg  19430  cntzsgrpcl  19462  cntzsubm  19466  cntrsubgnsg  19471  lactghmga  19533  symgfixf1  19565  odf1  19690  sylow1lem2  19727  sylow2blem2  19749  sylow3lem1  19755  lsmssv  19771  smndlsmidm  19784  pj1eu  19824  efglem  19844  efgtf  19850  efgred  19876  efgredeu  19880  frgpmhm  19893  frgpuptf  19898  frgpuplem  19900  mulgmhm  19955  ghmcmn  19959  invghm  19961  ablnsg  19975  imasabl  20004  cygabl  20019  gsum2d2lem  20101  gsum2d2  20102  gsumcom2  20103  dprd2d2  20174  ablfaclem2  20216  srgfcl  20336  srgcom4lem  20353  srglmhm  20361  srgrmhm  20362  ringcomlem  20421  isrnghm2d  20592  c0mgm  20601  c0mhm  20602  isrhm2d  20633  subrngringnsg  20716  issubrng2  20721  subrngint  20723  issubrg2  20755  subrgint  20758  rnghmsscmap2  20792  rnghmsscmap  20793  rnghmsubcsetclem2  20795  rhmsscmap2  20821  rhmsscmap  20822  rhmsubcsetclem2  20824  rhmsscrnghm  20828  rhmsubcrngclem2  20830  srhmsubc  20843  rhmsubc  20852  fldhmsubc  20952  primefld  20972  abvn0b  21003  suborng  21043  islmodd  21051  lmodscaf  21069  lmodprop2d  21109  islssd  21120  islss4  21147  lssacs  21152  lsspropd  21202  islmhmd  21224  lmhmima  21232  lmhmpreima  21233  reslmhm  21237  lspextmo  21241  lsmcl  21268  pj1lmhm  21285  islbs2  21342  issubrgd  21374  dflidl2rng  21407  rnglidlmmgm  21443  rhmpreimaidl  21480  rngqiprnglin  21506  prmidl2  21530  idlmulssprm  21531  isprmidlc  21536  rhmpreimaprmidl  21543  qsidomlem1  21544  qsidomlem2  21545  ssdifidllem  21548  ssdifidlprm  21550  prmidlsubm  21551  expmhm  21650  nn0srg  21651  prmirredlem  21686  expghm  21689  mulgghm2  21690  domnchr  21746  znf1o  21765  zntoslem  21770  znfld  21774  cygznlem3  21783  phlipf  21866  dsmmlss  21958  uvcf1  22006  frlmlbs  22011  lindff1  22034  lindfrn  22035  f1lindf  22036  issubassa2  22108  mvrf1  22201  mplsubglem  22214  mplsubrg  22220  mplcoe5lem  22256  mplcoe2  22258  mplind  22287  evlslem2  22296  evlseu  22300  mhplss  22384  ply1sclf1  22516  evls1maplmhm  22603  mamucl  22624  mamuass  22625  mamudi  22626  mamudir  22627  mamuvs1  22628  mamuvs2  22629  matbas2d  22646  mamumat1cl  22662  mamulid  22664  mamurid  22665  mat1mhm  22707  dmatid  22718  dmatsubcl  22721  dmatsgrp  22722  dmatmulcl  22723  dmatsrng  22724  dmatcrng  22725  scmatscmiddistr  22731  scmatscm  22736  scmatsgrp  22742  scmatsrng  22743  scmatcrng  22744  scmatsgrp1  22745  scmatsrng1  22746  scmatf1  22754  scmatmhm  22757  mavmul0g  22776  mdet1  22824  mdetunilem9  22843  mdetuni0  22844  mdetmul  22846  madutpos  22865  smadiadetlem4  22892  1elcpmat  22941  cpmatacl  22942  cpmatmcl  22945  mat2pmatf1  22955  mat2pmatmul  22957  mat2pmat1  22958  mat2pmatlin  22961  m2cpm  22967  m2cpminvid  22979  m2cpminvid2  22981  decpmatmul  22998  pmatcollpw1  23002  monmatcollpw  23005  pmatcollpw  23007  pmatcollpw3lem  23009  pmatcollpwscmatlem2  23016  pm2mpf1  23025  mp2pm2mplem4  23035  pm2mpmhmlem2  23045  chp0mat  23072  chpidmat  23073  tgclb  23196  mretopd  23318  toponmre  23319  iscldtop  23321  ordtbaslem  23414  ordtbas2  23417  cnt0  23572  haust1  23578  cnhaus  23580  isreg2  23603  dishaus  23608  ordthaus  23610  dfconn2  23645  iunconn  23654  clsconn  23656  2ndcomap  23685  dis2ndc  23687  llynlly  23704  restnlly  23709  restlly  23710  islly2  23711  llyidm  23715  nllyidm  23716  hausllycmp  23721  kgentopon  23765  txbas  23794  ptbasin2  23805  ptbasfi  23808  txcnp  23847  txcnmpt  23851  pthaus  23865  tx1stc  23877  xkococnlem  23886  xkococn  23887  cnmpt21  23898  qtoptop2  23926  qtopeu  23943  kqt0lem  23963  isr0  23964  regr1lem2  23967  kqreglem1  23968  kqreglem2  23969  kqnrmlem1  23970  kqnrmlem2  23971  nrmr0reg  23976  reghmph  24020  nrmhmph  24021  txswaphmeo  24032  qtophmeo  24044  fbun  24067  trfbas2  24070  isfil2  24083  infil  24090  trfil2  24114  filssufilg  24138  hausflim  24208  fclsnei  24246  fclsfnflim  24254  flimfnfcls  24255  ptcmplem1  24279  clssubg  24336  tgpconncomp  24340  qustgplem  24348  tsmsfbas  24355  utoptop  24461  iducn  24509  cstucnd  24510  isxmetd  24553  isxmet2d  24554  xmettpos  24576  prdsdsf  24594  prdsmet  24597  ressprdsds  24598  imasdsf1olem  24600  imasf1oxmet  24602  imasf1omet  24603  blfvalps  24610  xmetresbl  24664  metss2  24739  comet  24740  stdbdmet  24743  stdbdmopn  24745  methaus  24747  met2ndci  24749  metustfbas  24784  nrmmetd  24801  subgngp  24862  ngptgp  24863  sranlm  24911  nlmvscnlem1  24913  nlmvscn  24914  nrginvrcn  24919  lssnlm  24928  nghmcn  24972  qtopbaslem  24985  reconn  25056  xmetdcn2  25065  metdscn  25084  metnrm  25090  elcncf1di  25124  cncfcdm  25127  mulc1cncf  25134  cncfco  25136  reparphti  25226  isncvsngpd  25379  tcphcph  25466  ipcnlem1  25474  ipcn  25475  iscfil3  25502  bcthlem5  25557  rrxmet  25637  minveclem3  25658  minveclem7  25664  ovolicc2lem4  25749  dyadmbl  25829  volcn  25835  itg1addlem1  25921  itg1addlem2  25926  itg1addlem4  25928  mbfi1fseqlem1  25944  mbfi1fseqlem3  25946  mbfi1fseqlem4  25947  mbfi1fseqlem5  25948  dvmptfsum  26203  c1liplem1  26224  dvgt0lem2  26231  ftc1a  26265  ply1domn  26350  ply1divmo  26362  fta1b  26398  ig1peu  26401  coeeu  26452  plydivalg  26530  aaliou2b  26578  ulmss  26634  ulmcn  26636  efif1olem4  26783  efsubm  26789  logccv  26901  logbmpt  27026  logbfval  27028  cvxcl  27222  basellem4  27321  fsumdvdscom  27422  musum  27428  mpodvdsmulf1o  27431  fsumdvdsmul  27432  dvdsmulf1o  27433  dchrelbasd  27476  dchrmulcl  27486  dchrinv  27498  lgsqrlem2  27584  lgsdchr  27592  lgseisenlem2  27613  lgsquadlem1  27617  lgsquadlem2  27618  2sqreulem4  27691  dchrisumlema  27725  dchrisumlem2  27727  chpdifbndlem2  27791  pntpbnd  27825  pntibndlem3  27829  sltsd  28034  oldbday  28167  addsprop  28242  mulcutlem  28397  divsmo  28450  om2noseqf1o  28567  om2noseqiso  28568  axtgcont  28811  tgjustc1  28817  tgjustc2  28818  tgsegconeu  28829  iscgrglt  28857  ercgrg  28860  idmot  28880  motco  28883  cnvmot  28884  motcgrg  28887  tgisline  28975  tghilberti2  28986  mirreu3  29006  mirmot  29027  ragperp  29072  foot  29077  mideu  29094  midf  29161  lmimot  29183  trgcopyeu  29193  prlngmolem1  29310  f1otrgds  29326  f1otrg  29328  f1otrge  29329  xmstrkgc  29343  brbtwn2  29363  axlowdimlem15  29414  axcontlem2  29423  axcontlem10  29431  eengtrkg  29444  eengtrkge  29445  numedglnl  29602  usgredgreu  29679  uspgredg2vtxeu  29681  uspgredg2v  29685  usgredg2v  29688  wlkswwlksf1o  30348  wwlksnextinj  30368  clwlkclwwlkf1  30481  clwwlkf1  30520  frcond4  30751  frgrncvvdeqlem8  30787  frgrncvvdeq  30790  frgrwopreglem4  30796  numclwwlk1lem2f1  30838  nrt2irr  30954  grpoinvf  31014  nvmf  31127  vacn  31176  nmcvcn  31177  smcnlem  31179  sspg  31210  ssps  31212  sspmlem  31214  0lno  31272  blocni  31287  ipblnfi  31337  minvecolem7  31365  unopf1o  32398  cnvunop  32400  unoplin  32402  counop  32403  hmopadj2  32423  hmoplin  32424  bralnfn  32430  lnopeq0i  32489  hmops  32502  hmopm  32503  hmopco  32505  lnconi  32515  cnlnadjlem2  32550  adjmul  32574  adjadd  32575  cdjreui  32914  disjxpin  33062  off2  33115  2ndresdju  33123  fnpreimac  33144  suppovss  33154  f1od2  33191  xrofsup  33239  s3f1  33391  odutos  33409  dfmgc2lem  33436  dfmgc2  33437  pwrssmgc  33441  mgcf1o  33444  mndlactf1  33467  mndractf1  33469  abliso  33476  symgcntz  33526  tocyccntz  33585  conjga  33611  fxpsubrg  33615  archiabllem1  33634  archiabllem2  33638  urpropd  33671  elrgspnlem2  33684  rlocf1  33715  rrgsubm  33725  subrdom  33726  ricdomn1  33730  xrge0slmod  33789  nsgmgc  33842  intlidl  33849  idlinsubrg  33860  rhmimaidl  33861  mxidlprm  33874  mxidlirredi  33875  ssmxidllem  33877  drnglring  33903  dflringlem2  33906  rsprprmprmidl  33933  rsprprmprmidlb  33934  rprmirred  33942  rprmirredb  33943  1arithufdlem4  33958  selvply1rhmlema  34029  selvply1rhmlem1  34031  mplidomlem  34038  extvfvcl  34047  mplvrpmga  34056  ply1degltdimlem  34133  ply1degltdim  34134  lindsun  34136  fedgmullem1  34140  fedgmullem2  34141  fedgmul  34142  lactlmhm  34145  assalactf1o  34146  minplyirred  34222  constrsdrg  34286  1smat1  34315  submateq  34320  madjusmdetlem3  34340  zart0  34390  pstmxmet  34408  ofcf  34614  ldgenpisys  34678  rossros  34692  inelcarsg  34823  sibfof  34852  sitmf  34864  hgt750lemb  35165  erdszelem4  35774  erdszelem9  35779  erdsze2lem2  35784  cnpconn  35810  pconnconn  35811  txpconn  35812  ptpconn  35813  cvxpconn  35822  cvxsconn  35823  iccllysconn  35830  cvmseu  35856  cvmliftmo  35864  cvmlift2lem5  35887  cvmlift2lem9  35891  mrsubff1  36094  elmrsubrn  36100  mrsubco  36101  msubff1  36136  mvhf1  36139  r1peuqusdeg1  36223  segconeu  36592  nmulprop  36771  nadddilem4  36804  fnessref  36977  neibastop1  36979  filnetlem3  37000  onsuct0  37061  weiunlem  37083  mh-inf3f1  37161  unblimceq0lem  37204  unbdqndv2  37209  knoppndv  37232  irrdiff  38079  fin2so  38362  lindsadd  38368  poimirlem4  38374  poimirlem13  38383  poimirlem14  38384  poimirlem26  38396  heicant  38405  mblfinlem2  38408  ftc1anc  38451  sdclem1  38494  isbnd3  38535  prdsbnd  38544  ismtycnv  38553  ismtyhmeolem  38555  ismtyres  38559  bfplem1  38573  bfplem2  38574  bfp  38575  rrnmet  38580  ismrer1  38589  iccbnd  38591  grpokerinj  38644  isdrngo2  38709  rngogrphom  38722  rngohomco  38725  rngoisocnv  38732  iscringd  38749  eqvreldisj1  39676  erprt  39747  lfl0f  39943  lkrlss  39969  lshpsmreu  39983  linepsubN  40626  pmapsub  40642  lautcnv  40964  lautco  40971  idltrn  41024  cdleme50f1  41417  cdleme50laut  41421  istendod  41636  dihf11  42141  dih1dimatlem  42203  lcfl7N  42375  lcfrlem9  42424  mapd1o  42522  hdmapf1oN  42739  hgmapf1oN  42777  fmpocos  43104  qsalrel  43109  rediveud  43319  imacrhmcl  43403  evlselv  43436  fsuppind  43437  nacsfix  43558  rmxypairf1o  43753  wepwsolem  43884  dnnumch3  43889  fnwe2  43895  mpaaeu  43992  idomsubgmo  44035  mon1psubm  44041  deg1mhm  44042  isotone1  44889  isotone2  44890  mnringmulrcld  45067  traxext  45801  disjxp1  45904  disjf1  46016  wessf1ornlem  46018  projf1o  46029  sumnnodd  46461  lptioo2  46462  lptioo1  46463  cncfshift  46703  cncfperiod  46708  dvnprodlem1  46775  fourierdlem42  46978  nnfoctbdjlem  47284  isomennd  47360  smflimlem6  47605  fsetsnf1  47941  cfsetsnfsetf1  47948  otiunsndisjX  48168  imasetpreimafvbijlemf1  48305  iccpartgt  48328  icceuelpart  48337  ichnreuop  48373  sprsymrelfolem2  48394  sprsymrelf  48396  prproropf1o  48408  reupr  48423  reuopreuprim  48427  uhgrimprop  48809  isuspgrim0lem  48810  upgrimtrls  48823  gpgprismgr4cycllem11  49022  opmpoismgm  49083  mgmplusgiopALT  49110  2zlidl  49156  rhmsubcALTV  49201  srhmsubcALTV  49241  fldhmsubcALTV  49249  lindslinindsimp1  49388  1arymaptf1  49573  2arymaptf1  49584  eqfnovd  49795  toslat  49909  catprsc  49940  catprsc2  49941  oppcendc  49945  invfn  49957  iinfssclem2  49982  iinfssc  49984  iinfsubc  49985  discsubc  49991  nelsubclem  49994  resccatlem  50000  funchomf  50024  imasubclem2  50032  imaidfu  50037  imasubc  50078  imassc  50080  imasubc3  50083  fthcomf  50084  idfth  50085  cofidfth  50089  upeu2  50099  isnatd  50150  swapfffth  50210  diag1f1  50234  diag2f1  50236  fucoppc  50337  isthincd  50363  isthincd2  50364  oppcthinco  50366  oppcthinendcALT  50368  functhinclem4  50374  functhincfun  50376  thincfth  50379  thincciso  50380  thinccisod  50381  functermc  50435  arweuthinc  50456  arweutermc  50457  diagffth  50465  funcsn  50468  0fucterm  50470  veronesematrowd  50815  veroquadmodzerod  50818