Theorem ralrimivva 3104

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3059

This theorem is referenced by:  disjord  5019  disjxiun  5028  otsndisj  5377  otiunsndisj  5378  swopo  5454  issod  5476  reuop  6126  fcof1  7057  fliftfund  7082  isof1oidb  7093  isof1oopb  7094  soisores  7096  soisoi  7097  isocnv  7099  f1oiso  7120  oveqrspc2v  7200  oprres  7335  caovclg  7359  caovcomg  7362  off  7445  caofrss  7463  caonncan  7468  dmmpog  7801  fnmpoovd  7811  fmpoco  7819  fsplitfpar  7843  poxp  7851  fvmpocurryd  7969  smo11  8033  smoiso2  8038  omsmo  8315  qsdisj2  8409  eroprf  8429  dom2lem  8598  omxpenlem  8670  xpf1o  8732  unxpdomlem3  8806  fofinf1o  8875  dffi3  8971  supmo  8992  infmo  9035  inf3lem6  9172  cantnf  9232  rankxplim  9384  fseqenlem1  9527  fodomacn  9559  iunfictbso  9617  cofsmo  9772  infpssrlem5  9810  enfin2i  9824  fin23lem23  9829  fin23lem27  9831  fin23lem28  9843  compssiso  9877  ltordlem  11246  cju  11715  axdc4uzlem  13445  seqcaopr2  13501  seqhomo  13512  wrd2ind  14177  cshf1  14264  s3sndisj  14419  s3iunsndisj  14420  climcn2  15043  addcn2  15044  mulcn2  15046  o1of2  15063  isercolllem1  15117  fsum2dlem  15221  fsumcom2  15225  fprodser  15398  fprod2dlem  15429  fprodcom2  15433  isprm6  16158  crth  16218  eulerthlem2  16222  vdwlem12  16431  cshwsdisj  16538  imasaddfnlem  16907  imasvscafn  16916  mreexexd  17025  iscatd  17050  oppccomfpropd  17104  isofn  17153  sectmon  17160  ssctr  17203  ssceq  17204  catsubcat  17217  issubc3  17227  fullsubc  17228  fullresc  17229  isfuncd  17243  idfucl  17259  cofucl  17266  funcres2b  17275  fulloppc  17300  fthoppc  17301  idffth  17311  cofull  17312  cofth  17313  ressffth  17316  setcmon  17462  setcepi  17463  resssetc  17467  resscatc  17484  catciso  17486  fthestrcsetc  17519  fullestrcsetc  17520  embedsetcestrclem  17526  fthsetcestrc  17534  fullsetcestrc  17535  evlfcl  17591  uncfcurf  17608  hofcl  17628  yonedalem3  17649  yonedainv  17650  yonffthlem  17651  yoniso  17654  isdrs2  17668  isposd  17684  pospropd  17863  poslubmo  17875  posglbmo  17876  mgmplusf  17981  issstrmgm  17982  opifismgm  17988  ismndd  18052  mndpropd  18055  issubmnd  18057  mndinvmod  18060  mhmpropd  18081  idmhm  18084  mhmf1o  18085  issubmd  18090  mndissubm  18091  0mhm  18103  resmhm  18104  resmhm2  18105  resmhm2b  18106  mhmco  18107  submacs  18110  prdspjmhm  18112  pwsdiagmhm  18114  pwsco1mhm  18115  pwsco2mhm  18116  gsumwspan  18130  frmdsssubm  18145  frmdup1  18148  grpsubf  18299  dfgrp3  18319  mhmmnd  18342  mhmfmhm  18343  issubg4  18419  grpissubg  18420  isnsg3  18433  nsgacs  18435  0nsg  18442  nsgid  18443  cycsubmcom  18468  isghmd  18488  ghmmhm  18489  idghm  18494  ghmnsgima  18503  ghmnsgpreima  18504  ghmf1  18508  ghmf1o  18509  gaid  18550  subgga  18551  gass  18552  gasubg  18553  cntzsubm  18587  cntrsubgnsg  18592  lactghmga  18654  symgfixf1  18686  odf1  18810  sylow1lem2  18845  sylow2blem2  18867  sylow3lem1  18873  lsmssv  18889  smndlsmidm  18902  lsmidmOLD  18910  pj1eu  18943  efglem  18963  efgtf  18969  efgred  18995  efgredeu  18999  frgpmhm  19012  frgpuptf  19017  frgpuplem  19019  mulgmhm  19070  ghmcmn  19074  invghm  19076  ablnsg  19089  cygabl  19132  gsum2d2lem  19215  gsum2d2  19216  gsumcom2  19217  dprd2d2  19288  ablfaclem2  19330  srgfcl  19387  srglmhm  19407  srgrmhm  19408  isrhm2d  19605  kerf1ghm  19620  issubrg2  19677  subrgint  19679  primefld  19706  islmodd  19762  lmodscaf  19778  lmodprop2d  19818  islssd  19829  islss4  19856  lssacs  19861  lsspropd  19911  islmhmd  19933  lmhmima  19941  lmhmpreima  19942  reslmhm  19946  lspextmo  19950  lsmcl  19977  pj1lmhm  19994  islbs2  20048  issubrngd2  20083  opprdomn  20196  abvn0b  20197  expmhm  20289  nn0srg  20290  prmirredlem  20316  expghm  20319  mulgghm2  20320  domnchr  20354  znf1o  20373  zntoslem  20378  znfld  20382  cygznlem3  20391  phlipf  20471  dsmmlss  20563  uvcf1  20611  frlmlbs  20616  lindff1  20639  lindfrn  20640  f1lindf  20641  issubassa2  20709  mvrf1  20807  mplsubglem  20818  mplsubrg  20824  mplcoe5lem  20853  mplcoe2  20855  mplind  20885  evlslem2  20896  evlseu  20900  mhplss  20952  ply1sclf1  21067  mamucl  21155  mamuass  21156  mamudi  21157  mamudir  21158  mamuvs1  21159  mamuvs2  21160  matbas2d  21177  mamumat1cl  21193  mamulid  21195  mamurid  21196  mat1mhm  21238  dmatid  21249  dmatsubcl  21252  dmatsgrp  21253  dmatmulcl  21254  dmatsrng  21255  dmatcrng  21256  scmatscmiddistr  21262  scmatscm  21267  scmatsgrp  21273  scmatsrng  21274  scmatcrng  21275  scmatsgrp1  21276  scmatsrng1  21277  scmatf1  21285  scmatmhm  21288  mavmul0g  21307  mdet1  21355  mdetunilem9  21374  mdetuni0  21375  mdetmul  21377  madutpos  21396  smadiadetlem4  21423  1elcpmat  21469  cpmatacl  21470  cpmatmcl  21473  mat2pmatf1  21483  mat2pmatmul  21485  mat2pmat1  21486  mat2pmatlin  21489  m2cpm  21495  m2cpminvid  21507  m2cpminvid2  21509  decpmatmul  21526  pmatcollpw1  21530  monmatcollpw  21533  pmatcollpw  21535  pmatcollpw3lem  21537  pmatcollpwscmatlem2  21544  pm2mpf1  21553  mp2pm2mplem4  21563  pm2mpmhmlem2  21573  chp0mat  21600  chpidmat  21601  tgclb  21724  mretopd  21846  toponmre  21847  iscldtop  21849  ordtbaslem  21942  ordtbas2  21945  cnt0  22100  haust1  22106  cnhaus  22108  isreg2  22131  dishaus  22136  ordthaus  22138  dfconn2  22173  iunconn  22182  clsconn  22184  2ndcomap  22212  dis2ndc  22214  llynlly  22231  restnlly  22236  restlly  22237  islly2  22238  llyidm  22242  nllyidm  22243  hausllycmp  22248  kgentopon  22292  txbas  22321  ptbasin2  22332  ptbasfi  22335  txcnp  22374  txcnmpt  22378  pthaus  22392  tx1stc  22404  xkococnlem  22413  xkococn  22414  cnmpt21  22425  qtoptop2  22453  qtopeu  22470  kqt0lem  22490  isr0  22491  regr1lem2  22494  kqreglem1  22495  kqreglem2  22496  kqnrmlem1  22497  kqnrmlem2  22498  nrmr0reg  22503  reghmph  22547  nrmhmph  22548  txswaphmeo  22559  qtophmeo  22571  fbun  22594  trfbas2  22597  isfil2  22610  infil  22617  trfil2  22641  filssufilg  22665  hausflim  22735  fclsnei  22773  fclsfnflim  22781  flimfnfcls  22782  ptcmplem1  22806  clssubg  22863  tgpconncomp  22867  qustgplem  22875  tsmsfbas  22882  utoptop  22989  iducn  23038  cstucnd  23039  isxmetd  23082  isxmet2d  23083  xmettpos  23105  prdsdsf  23123  prdsmet  23126  ressprdsds  23127  imasdsf1olem  23129  imasf1oxmet  23131  imasf1omet  23132  blfvalps  23139  xmetresbl  23193  metss2  23268  comet  23269  stdbdmet  23272  stdbdmopn  23274  methaus  23276  met2ndci  23278  metustfbas  23313  nrmmetd  23330  subgngp  23391  ngptgp  23392  sranlm  23440  nlmvscnlem1  23442  nlmvscn  23443  nrginvrcn  23448  lssnlm  23457  nghmcn  23501  qtopbaslem  23514  reconn  23583  xmetdcn2  23592  metdscn  23611  metnrm  23617  elcncf1di  23650  cncffvrn  23653  mulc1cncf  23660  cncfco  23662  reparphti  23752  isncvsngpd  23905  tcphcph  23992  ipcnlem1  24000  ipcn  24001  iscfil3  24028  bcthlem5  24083  rrxmet  24163  minveclem3  24184  minveclem7  24190  ovolicc2lem4  24275  dyadmbl  24355  volcn  24361  itg1addlem1  24447  itg1addlem2  24452  itg1addlem4  24454  itg1addlem4OLD  24455  mbfi1fseqlem1  24471  mbfi1fseqlem3  24473  mbfi1fseqlem4  24474  mbfi1fseqlem5  24475  dvmptfsum  24730  c1liplem1  24751  dvgt0lem2  24758  ftc1a  24792  ply1domn  24879  ply1divmo  24891  fta1b  24925  ig1peu  24927  coeeu  24977  plydivalg  25050  aaliou2b  25092  ulmss  25147  ulmcn  25149  efif1olem4  25292  efsubm  25298  logccv  25409  logbmpt  25529  logbfval  25531  cvxcl  25725  basellem4  25824  fsumdvdscom  25925  musum  25931  dvdsmulf1o  25934  fsumdvdsmul  25935  dchrelbasd  25978  dchrmulcl  25988  dchrinv  26000  lgsqrlem2  26086  lgsdchr  26094  lgseisenlem2  26115  lgsquadlem1  26119  lgsquadlem2  26120  2sqreulem4  26193  dchrisumlema  26227  dchrisumlem2  26229  chpdifbndlem2  26293  pntpbnd  26327  pntibndlem3  26331  axtgcont  26418  tgjustc1  26424  tgjustc2  26425  iscgrglt  26463  ercgrg  26466  idmot  26486  motco  26489  cnvmot  26490  motcgrg  26493  tgisline  26576  tghilberti2  26587  mirreu3  26603  mirmot  26624  ragperp  26666  foot  26671  mideu  26687  midf  26725  lmimot  26747  trgcopyeu  26755  f1otrgds  26818  f1otrg  26820  f1otrge  26821  xmstrkgc  26835  brbtwn2  26854  axlowdimlem15  26905  axcontlem2  26914  axcontlem10  26922  eengtrkg  26935  eengtrkge  26936  numedglnl  27092  usgredgreu  27163  uspgredg2vtxeu  27165  uspgredg2v  27169  usgredg2v  27172  wlkswwlksf1o  27820  wwlksnextinj  27840  clwlkclwwlkf1  27950  clwwlkf1  27989  frcond4  28210  frgrncvvdeqlem8  28246  frgrncvvdeq  28249  frgrwopreglem4  28255  numclwwlk1lem2f1  28297  grpoinvf  28470  nvmf  28583  vacn  28632  nmcvcn  28633  smcnlem  28635  sspg  28666  ssps  28668  sspmlem  28670  0lno  28728  blocni  28743  ipblnfi  28793  minvecolem7  28821  unopf1o  29854  cnvunop  29856  unoplin  29858  counop  29859  hmopadj2  29879  hmoplin  29880  bralnfn  29886  lnopeq0i  29945  hmops  29958  hmopm  29959  hmopco  29961  lnconi  29971  cnlnadjlem2  30006  adjmul  30030  adjadd  30031  cdjreui  30370  disjxpin  30504  off2  30555  2ndresdju  30563  fnpreimac  30586  suppovss  30595  f1od2  30634  xrofsup  30668  s3f1  30799  ccatf1  30801  swrdf1  30806  odutos  30826  dfmgc2lem  30853  dfmgc2  30854  pwrssmgc  30858  mgcf1o  30861  abliso  30885  symgcntz  30934  tocyccntz  30991  archiabllem1  31027  archiabllem2  31031  suborng  31094  xrge0slmod  31123  nsgmgc  31172  intlidl  31177  rhmpreimaidl  31178  idlinsubrg  31183  rhmimaidl  31184  prmidl2  31191  idlmulssprm  31192  isprmidlc  31198  rhmpreimaprmidl  31202  qsidomlem1  31203  qsidomlem2  31204  mxidlprm  31215  ssmxidllem  31216  lindsun  31281  fedgmullem1  31285  fedgmullem2  31286  fedgmul  31287  1smat1  31329  submateq  31334  madjusmdetlem3  31354  zart0  31404  pstmxmet  31422  ofcf  31644  ldgenpisys  31707  rossros  31721  inelcarsg  31851  sibfof  31880  sitmf  31892  hgt750lemb  32209  erdszelem4  32730  erdszelem9  32735  erdsze2lem2  32740  cnpconn  32766  pconnconn  32767  txpconn  32768  ptpconn  32769  cvxpconn  32778  cvxsconn  32779  iccllysconn  32786  cvmseu  32812  cvmliftmo  32820  cvmlift2lem5  32843  cvmlift2lem9  32847  mrsubff1  33050  elmrsubrn  33056  mrsubco  33057  msubff1  33092  mvhf1  33095  ssltd  33632  oldbday  33727  segconeu  33959  fnessref  34192  neibastop1  34194  filnetlem3  34215  onsuct0  34276  unblimceq0lem  34332  unbdqndv2  34337  knoppndv  34360  irrdiff  35140  uncf  35402  fin2so  35410  lindsadd  35416  poimirlem4  35427  poimirlem13  35436  poimirlem14  35437  poimirlem26  35449  heicant  35458  mblfinlem2  35461  ftc1anc  35504  sdclem1  35547  isbnd3  35588  prdsbnd  35597  ismtycnv  35606  ismtyhmeolem  35608  ismtyres  35612  bfplem1  35626  bfplem2  35627  bfp  35628  rrnmet  35633  ismrer1  35642  iccbnd  35644  grpokerinj  35697  isdrngo2  35762  rngogrphom  35775  rngohomco  35778  rngoisocnv  35785  iscringd  35802  erprt  36533  lfl0f  36729  lkrlss  36755  lshpsmreu  36769  linepsubN  37412  pmapsub  37428  lautcnv  37750  lautco  37757  idltrn  37810  cdleme50f1  38203  cdleme50laut  38207  istendod  38422  dihf11  38927  dih1dimatlem  38989  lcfl7N  39161  lcfrlem9  39210  mapd1o  39308  hdmapf1oN  39525  hgmapf1oN  39563  qsalrel  39820  ismhmd  39843  fsuppind  39881  sn-negex12  39998  nacsfix  40129  rmxypairf1o  40328  wepwsolem  40462  dnnumch3  40467  fnwe2  40473  mpaaeu  40570  idomsubgmo  40618  mon1psubm  40626  deg1mhm  40627  isotone1  41227  isotone2  41228  mnringmulrcld  41411  disjxp1  42178  disjf1  42281  wessf1ornlem  42283  projf1o  42297  sumnnodd  42736  lptioo2  42737  lptioo1  42738  cncfshift  42980  cncfperiod  42985  dvnprodlem1  43052  fourierdlem42  43255  nnfoctbdjlem  43558  isomennd  43634  smflimlem6  43873  fsetsnf1  44108  cfsetsnfsetf1  44115  otiunsndisjX  44334  imasetpreimafvbijlemf1  44420  iccpartgt  44443  icceuelpart  44452  ichnreuop  44488  sprsymrelfolem2  44509  sprsymrelf  44511  prproropf1o  44523  reupr  44538  reuopreuprim  44542  isomuspgrlem2c  44846  isomuspgr  44850  ismgmd  44894  mgmhmpropd  44903  mgmhmf1o  44905  idmgmhm  44906  issubmgm2  44908  rabsubmgmd  44909  resmgmhm  44916  resmgmhm2  44917  resmgmhm2b  44918  mgmhmco  44919  submgmacs  44922  opmpoismgm  44925  mgmplusgiopALT  44952  isrnghm2d  45023  c0mgm  45031  c0mhm  45032  lidlmmgm  45047  2zlidl  45056  rnghmsscmap2  45095  rnghmsscmap  45096  rnghmsubcsetclem2  45098  rhmsscmap2  45141  rhmsscmap  45142  rhmsubcsetclem2  45144  rhmsscrnghm  45148  rhmsubcrngclem2  45150  srhmsubc  45198  fldhmsubc  45206  rhmsubc  45212  srhmsubcALTV  45216  fldhmsubcALTV  45224  rhmsubcALTV  45230  lindslinindsimp1  45362  1arymaptf1  45552  2arymaptf1  45563  catprsc  45805  catprsc2  45806  isthincd  45821  isthincd2  45822