Theorem ralrimivva 3201

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  disjord  5137  disjxiun  5146  otsndisj  5520  otiunsndisj  5521  swopo  5600  issod  5622  reuop  6293  fcof1  7285  fliftfund  7310  isof1oidb  7321  isof1oopb  7322  soisores  7324  soisoi  7325  isocnv  7327  f1oiso  7348  oveqrspc2v  7436  oprres  7575  caovclg  7599  caovcomg  7602  off  7688  caofrss  7706  caonncan  7711  dmmpog  8061  fnmpoovd  8073  fmpoco  8081  fsplitfpar  8104  poxp  8114  fvmpocurryd  8256  smo11  8364  smoiso2  8369  omsmo  8657  nnasmo  8662  coflton  8670  qsdisj2  8789  eroprf  8809  dom2lem  8988  omxpenlem  9073  xpf1o  9139  unxpdomlem3  9252  fofinf1o  9327  dffi3  9426  supmo  9447  infmo  9490  inf3lem6  9628  cantnf  9688  rankxplim  9874  fseqenlem1  10019  fodomacn  10051  iunfictbso  10109  cofsmo  10264  infpssrlem5  10302  enfin2i  10316  fin23lem23  10321  fin23lem27  10323  fin23lem28  10335  compssiso  10369  ltordlem  11739  cju  12208  axdc4uzlem  13948  seqcaopr2  14004  seqhomo  14015  wrd2ind  14673  cshf1  14760  s3sndisj  14914  s3iunsndisj  14915  climcn2  15537  addcn2  15538  mulcn2  15540  o1of2  15557  isercolllem1  15611  fsum2dlem  15716  fsumcom2  15720  fprodser  15893  fprod2dlem  15924  fprodcom2  15928  isprm6  16651  crth  16711  eulerthlem2  16715  vdwlem12  16925  cshwsdisj  17032  imasaddfnlem  17474  imasvscafn  17483  mreexexd  17592  iscatd  17617  oppccomfpropd  17673  isofn  17722  sectmon  17729  ssctr  17772  ssceq  17773  catsubcat  17789  issubc3  17799  fullsubc  17800  fullresc  17801  isfuncd  17815  idfucl  17831  cofucl  17838  funcres2b  17847  fulloppc  17873  fthoppc  17874  idffth  17884  cofull  17885  cofth  17886  ressffth  17889  setcmon  18037  setcepi  18038  resssetc  18042  resscatc  18059  catciso  18061  fthestrcsetc  18102  fullestrcsetc  18103  embedsetcestrclem  18109  fthsetcestrc  18117  fullsetcestrc  18118  evlfcl  18175  uncfcurf  18192  hofcl  18212  yonedalem3  18233  yonedainv  18234  yonffthlem  18235  yoniso  18238  isdrs2  18259  isposd  18276  pospropd  18280  poslubmo  18364  posglbmo  18365  mgmplusf  18571  issstrmgm  18572  opifismgm  18578  issgrpd  18621  sgrppropd  18622  ismndd  18647  mndpropd  18650  issubmnd  18652  mndinvmod  18655  ismhmd  18674  mhmpropd  18678  idmhm  18681  mhmf1o  18682  issubmd  18687  mndissubm  18688  0mhm  18700  resmhm  18701  resmhm2  18702  resmhm2b  18703  mhmco  18704  submacs  18708  prdspjmhm  18710  pwsdiagmhm  18712  pwsco1mhm  18713  pwsco2mhm  18714  gsumwspan  18727  frmdsssubm  18742  frmdup1  18745  grpsubf  18902  dfgrp3  18922  mhmmnd  18947  mhmfmhm  18948  issubg4  19025  grpissubg  19026  isnsg3  19040  nsgacs  19042  0nsg  19049  nsgid  19050  qus0subgadd  19076  cycsubmcom  19081  isghmd  19101  ghmmhm  19102  idghm  19107  ghmnsgima  19116  ghmnsgpreima  19117  ghmf1  19121  ghmf1o  19122  gaid  19163  subgga  19164  gass  19165  gasubg  19166  cntzsgrpcl  19198  cntzsubm  19202  cntrsubgnsg  19207  lactghmga  19273  symgfixf1  19305  odf1  19430  sylow1lem2  19467  sylow2blem2  19489  sylow3lem1  19495  lsmssv  19511  smndlsmidm  19524  pj1eu  19564  efglem  19584  efgtf  19590  efgred  19616  efgredeu  19620  frgpmhm  19633  frgpuptf  19638  frgpuplem  19640  mulgmhm  19695  ghmcmn  19699  invghm  19701  ablnsg  19715  imasabl  19744  cygabl  19759  gsum2d2lem  19841  gsum2d2  19842  gsumcom2  19843  dprd2d2  19914  ablfaclem2  19956  srgfcl  20019  srgcom4lem  20036  srglmhm  20044  srgrmhm  20045  ringcomlem  20096  isrhm2d  20265  kerf1ghm  20282  issubrg2  20339  subrgint  20342  primefld  20421  islmodd  20477  lmodscaf  20494  lmodprop2d  20534  islssd  20546  islss4  20573  lssacs  20578  lsspropd  20628  islmhmd  20650  lmhmima  20658  lmhmpreima  20659  reslmhm  20663  lspextmo  20667  lsmcl  20694  pj1lmhm  20711  islbs2  20767  issubrgd  20811  dflidl2  20843  opprdomn  20919  abvn0b  20920  expmhm  21014  nn0srg  21015  prmirredlem  21042  expghm  21045  mulgghm2  21046  domnchr  21084  znf1o  21107  zntoslem  21112  znfld  21116  cygznlem3  21125  phlipf  21205  dsmmlss  21299  uvcf1  21347  frlmlbs  21352  lindff1  21375  lindfrn  21376  f1lindf  21377  issubassa2  21446  mvrf1  21545  mplsubglem  21558  mplsubrg  21564  mplcoe5lem  21594  mplcoe2  21596  mplind  21631  evlslem2  21642  evlseu  21646  mhplss  21698  ply1sclf1  21811  mamucl  21901  mamuass  21902  mamudi  21903  mamudir  21904  mamuvs1  21905  mamuvs2  21906  matbas2d  21925  mamumat1cl  21941  mamulid  21943  mamurid  21944  mat1mhm  21986  dmatid  21997  dmatsubcl  22000  dmatsgrp  22001  dmatmulcl  22002  dmatsrng  22003  dmatcrng  22004  scmatscmiddistr  22010  scmatscm  22015  scmatsgrp  22021  scmatsrng  22022  scmatcrng  22023  scmatsgrp1  22024  scmatsrng1  22025  scmatf1  22033  scmatmhm  22036  mavmul0g  22055  mdet1  22103  mdetunilem9  22122  mdetuni0  22123  mdetmul  22125  madutpos  22144  smadiadetlem4  22171  1elcpmat  22217  cpmatacl  22218  cpmatmcl  22221  mat2pmatf1  22231  mat2pmatmul  22233  mat2pmat1  22234  mat2pmatlin  22237  m2cpm  22243  m2cpminvid  22255  m2cpminvid2  22257  decpmatmul  22274  pmatcollpw1  22278  monmatcollpw  22281  pmatcollpw  22283  pmatcollpw3lem  22285  pmatcollpwscmatlem2  22292  pm2mpf1  22301  mp2pm2mplem4  22311  pm2mpmhmlem2  22321  chp0mat  22348  chpidmat  22349  tgclb  22473  mretopd  22596  toponmre  22597  iscldtop  22599  ordtbaslem  22692  ordtbas2  22695  cnt0  22850  haust1  22856  cnhaus  22858  isreg2  22881  dishaus  22886  ordthaus  22888  dfconn2  22923  iunconn  22932  clsconn  22934  2ndcomap  22962  dis2ndc  22964  llynlly  22981  restnlly  22986  restlly  22987  islly2  22988  llyidm  22992  nllyidm  22993  hausllycmp  22998  kgentopon  23042  txbas  23071  ptbasin2  23082  ptbasfi  23085  txcnp  23124  txcnmpt  23128  pthaus  23142  tx1stc  23154  xkococnlem  23163  xkococn  23164  cnmpt21  23175  qtoptop2  23203  qtopeu  23220  kqt0lem  23240  isr0  23241  regr1lem2  23244  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  nrmr0reg  23253  reghmph  23297  nrmhmph  23298  txswaphmeo  23309  qtophmeo  23321  fbun  23344  trfbas2  23347  isfil2  23360  infil  23367  trfil2  23391  filssufilg  23415  hausflim  23485  fclsnei  23523  fclsfnflim  23531  flimfnfcls  23532  ptcmplem1  23556  clssubg  23613  tgpconncomp  23617  qustgplem  23625  tsmsfbas  23632  utoptop  23739  iducn  23788  cstucnd  23789  isxmetd  23832  isxmet2d  23833  xmettpos  23855  prdsdsf  23873  prdsmet  23876  ressprdsds  23877  imasdsf1olem  23879  imasf1oxmet  23881  imasf1omet  23882  blfvalps  23889  xmetresbl  23943  metss2  24021  comet  24022  stdbdmet  24025  stdbdmopn  24027  methaus  24029  met2ndci  24031  metustfbas  24066  nrmmetd  24083  subgngp  24144  ngptgp  24145  sranlm  24201  nlmvscnlem1  24203  nlmvscn  24204  nrginvrcn  24209  lssnlm  24218  nghmcn  24262  qtopbaslem  24275  reconn  24344  xmetdcn2  24353  metdscn  24372  metnrm  24378  elcncf1di  24411  cncfcdm  24414  mulc1cncf  24421  cncfco  24423  reparphti  24513  isncvsngpd  24667  tcphcph  24754  ipcnlem1  24762  ipcn  24763  iscfil3  24790  bcthlem5  24845  rrxmet  24925  minveclem3  24946  minveclem7  24952  ovolicc2lem4  25037  dyadmbl  25117  volcn  25123  itg1addlem1  25209  itg1addlem2  25214  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  dvmptfsum  25492  c1liplem1  25513  dvgt0lem2  25520  ftc1a  25554  ply1domn  25641  ply1divmo  25653  fta1b  25687  ig1peu  25689  coeeu  25739  plydivalg  25812  aaliou2b  25854  ulmss  25909  ulmcn  25911  efif1olem4  26054  efsubm  26060  logccv  26171  logbmpt  26293  logbfval  26295  cvxcl  26489  basellem4  26588  fsumdvdscom  26689  musum  26695  dvdsmulf1o  26698  fsumdvdsmul  26699  dchrelbasd  26742  dchrmulcl  26752  dchrinv  26764  lgsqrlem2  26850  lgsdchr  26858  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  2sqreulem4  26957  dchrisumlema  26991  dchrisumlem2  26993  chpdifbndlem2  27057  pntpbnd  27091  pntibndlem3  27095  ssltd  27293  oldbday  27395  addsprop  27460  mulscutlem  27587  divsmo  27634  axtgcont  27720  tgjustc1  27726  tgjustc2  27727  iscgrglt  27765  ercgrg  27768  idmot  27788  motco  27791  cnvmot  27792  motcgrg  27795  tgisline  27878  tghilberti2  27889  mirreu3  27905  mirmot  27926  ragperp  27968  foot  27973  mideu  27989  midf  28027  lmimot  28049  trgcopyeu  28057  f1otrgds  28120  f1otrg  28122  f1otrge  28123  xmstrkgc  28143  brbtwn2  28163  axlowdimlem15  28214  axcontlem2  28223  axcontlem10  28231  eengtrkg  28244  eengtrkge  28245  numedglnl  28404  usgredgreu  28475  uspgredg2vtxeu  28477  uspgredg2v  28481  usgredg2v  28484  wlkswwlksf1o  29133  wwlksnextinj  29153  clwlkclwwlkf1  29263  clwwlkf1  29302  frcond4  29523  frgrncvvdeqlem8  29559  frgrncvvdeq  29562  frgrwopreglem4  29568  numclwwlk1lem2f1  29610  nrt2irr  29726  grpoinvf  29785  nvmf  29898  vacn  29947  nmcvcn  29948  smcnlem  29950  sspg  29981  ssps  29983  sspmlem  29985  0lno  30043  blocni  30058  ipblnfi  30108  minvecolem7  30136  unopf1o  31169  cnvunop  31171  unoplin  31173  counop  31174  hmopadj2  31194  hmoplin  31195  bralnfn  31201  lnopeq0i  31260  hmops  31273  hmopm  31274  hmopco  31276  lnconi  31286  cnlnadjlem2  31321  adjmul  31345  adjadd  31346  cdjreui  31685  disjxpin  31819  off2  31866  2ndresdju  31874  fnpreimac  31896  suppovss  31906  f1od2  31946  xrofsup  31980  s3f1  32113  ccatf1  32115  swrdf1  32120  odutos  32138  dfmgc2lem  32165  dfmgc2  32166  pwrssmgc  32170  mgcf1o  32173  abliso  32197  symgcntz  32246  tocyccntz  32303  archiabllem1  32339  archiabllem2  32343  urpropd  32378  suborng  32433  xrge0slmod  32463  nsgmgc  32523  intlidl  32536  rhmpreimaidl  32537  idlinsubrg  32549  rhmimaidl  32550  prmidl2  32559  idlmulssprm  32560  isprmidlc  32566  rhmpreimaprmidl  32570  qsidomlem1  32571  qsidomlem2  32572  mxidlprm  32586  mxidlirredi  32587  ssmxidllem  32589  ply1degltdimlem  32707  ply1degltdim  32708  lindsun  32710  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  evls1maplmhm  32760  minplyirred  32770  1smat1  32784  submateq  32789  madjusmdetlem3  32809  zart0  32859  pstmxmet  32877  ofcf  33101  ldgenpisys  33164  rossros  33178  inelcarsg  33310  sibfof  33339  sitmf  33351  hgt750lemb  33668  erdszelem4  34185  erdszelem9  34190  erdsze2lem2  34195  cnpconn  34221  pconnconn  34222  txpconn  34223  ptpconn  34224  cvxpconn  34233  cvxsconn  34234  iccllysconn  34241  cvmseu  34267  cvmliftmo  34275  cvmlift2lem5  34298  cvmlift2lem9  34302  mrsubff1  34505  elmrsubrn  34511  mrsubco  34512  msubff1  34547  mvhf1  34550  segconeu  34983  gg-reparphti  35172  fnessref  35242  neibastop1  35244  filnetlem3  35265  onsuct0  35326  unblimceq0lem  35382  unbdqndv2  35387  knoppndv  35410  irrdiff  36207  uncf  36467  fin2so  36475  lindsadd  36481  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  poimirlem26  36514  heicant  36523  mblfinlem2  36526  ftc1anc  36569  sdclem1  36611  isbnd3  36652  prdsbnd  36661  ismtycnv  36670  ismtyhmeolem  36672  ismtyres  36676  bfplem1  36690  bfplem2  36691  bfp  36692  rrnmet  36697  ismrer1  36706  iccbnd  36708  grpokerinj  36761  isdrngo2  36826  rngogrphom  36839  rngohomco  36842  rngoisocnv  36849  iscringd  36866  eqvreldisj1  37694  erprt  37743  lfl0f  37939  lkrlss  37965  lshpsmreu  37979  linepsubN  38623  pmapsub  38639  lautcnv  38961  lautco  38968  idltrn  39021  cdleme50f1  39414  cdleme50laut  39418  istendod  39633  dihf11  40138  dih1dimatlem  40200  lcfl7N  40372  lcfrlem9  40421  mapd1o  40519  hdmapf1oN  40736  hgmapf1oN  40774  fmpocos  41056  qsalrel  41062  imacrhmcl  41089  evlselv  41159  fsuppind  41162  sn-negex12  41289  nacsfix  41450  rmxypairf1o  41650  wepwsolem  41784  dnnumch3  41789  fnwe2  41795  mpaaeu  41892  idomsubgmo  41940  mon1psubm  41948  deg1mhm  41949  isotone1  42799  isotone2  42800  mnringmulrcld  42987  disjxp1  43756  disjf1  43880  wessf1ornlem  43882  projf1o  43896  sumnnodd  44346  lptioo2  44347  lptioo1  44348  cncfshift  44590  cncfperiod  44595  dvnprodlem1  44662  fourierdlem42  44865  nnfoctbdjlem  45171  isomennd  45247  smflimlem6  45492  fsetsnf1  45762  cfsetsnfsetf1  45769  otiunsndisjX  45987  imasetpreimafvbijlemf1  46072  iccpartgt  46095  icceuelpart  46104  ichnreuop  46140  sprsymrelfolem2  46161  sprsymrelf  46163  prproropf1o  46175  reupr  46190  reuopreuprim  46194  isomuspgrlem2c  46498  isomuspgr  46502  ismgmd  46546  mgmhmpropd  46555  mgmhmf1o  46557  idmgmhm  46558  issubmgm2  46560  rabsubmgmd  46561  resmgmhm  46568  resmgmhm2  46569  resmgmhm2b  46570  mgmhmco  46571  submgmacs  46574  opmpoismgm  46577  mgmplusgiopALT  46604  isrnghm2d  46699  c0mgm  46708  c0mhm  46709  subrngringnsg  46732  issubrng2  46737  subrngint  46739  dflidl2rng  46750  rnglidlmmgm  46756  rngqiprnglin  46787  2zlidl  46832  rnghmsscmap2  46871  rnghmsscmap  46872  rnghmsubcsetclem2  46874  rhmsscmap2  46917  rhmsscmap  46918  rhmsubcsetclem2  46920  rhmsscrnghm  46924  rhmsubcrngclem2  46926  srhmsubc  46974  fldhmsubc  46982  rhmsubc  46988  srhmsubcALTV  46992  fldhmsubcALTV  47000  rhmsubcALTV  47006  lindslinindsimp1  47138  1arymaptf1  47328  2arymaptf1  47339  toslat  47607  catprsc  47633  catprsc2  47634  isthincd  47657  isthincd2  47658  functhinclem4  47664  thincfth  47668  thincciso  47669