Theorem ralrimivva 3178

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  disjord  5091  disjxiun  5099  otsndisj  5474  otiunsndisj  5475  swopo  5550  issod  5574  reuop  6255  fcof1  7245  fliftfund  7271  isof1oidb  7282  isof1oopb  7283  soisores  7285  soisoi  7286  isocnv  7288  f1oiso  7309  oveqrspc2v  7397  oprres  7538  caovclg  7562  caovcomg  7565  off  7652  coof  7658  caofidlcan  7672  caofrss  7673  caonncan  7678  dmmpog  8033  fnmpoovd  8044  fmpoco  8052  fsplitfpar  8075  poxp  8085  fvmpocurryd  8228  smo11  8311  smoiso2  8316  omsmo  8600  nnasmo  8605  coflton  8613  qsdisj2  8746  eroprf  8766  dom2lem  8941  omxpenlem  9020  xpf1o  9081  unxpdomlem3  9176  fofinf1o  9260  dffi3  9359  supmo  9380  infmo  9425  inf3lem6  9565  cantnf  9625  rankxplim  9811  fseqenlem1  9956  fodomacn  9988  iunfictbso  10046  cofsmo  10201  infpssrlem5  10239  enfin2i  10253  fin23lem23  10258  fin23lem27  10260  fin23lem28  10272  compssiso  10306  ltordlem  11682  cju  12161  axdc4uzlem  13927  seqcaopr2  13982  seqhomo  13993  wrd2ind  14666  cshf1  14753  s3sndisj  14911  s3iunsndisj  14912  climcn2  15537  addcn2  15538  mulcn2  15540  o1of2  15557  isercolllem1  15609  fsum2dlem  15714  fsumcom2  15718  fprodser  15893  fprod2dlem  15924  fprodcom2  15928  isprm6  16662  crth  16726  eulerthlem2  16730  vdwlem12  16941  cshwsdisj  17047  imasaddfnlem  17469  imasvscafn  17478  mreexexd  17591  iscatd  17616  oppccomfpropd  17670  isofn  17719  sectmon  17726  ssctr  17769  ssceq  17770  catsubcat  17783  issubc3  17793  fullsubc  17794  fullresc  17795  isfuncd  17809  idfucl  17825  cofucl  17832  funcres2b  17841  fulloppc  17868  fthoppc  17869  idffth  17879  cofull  17880  cofth  17881  ressffth  17884  setcmon  18031  setcepi  18032  resssetc  18036  resscatc  18053  catciso  18055  fthestrcsetc  18093  fullestrcsetc  18094  embedsetcestrclem  18100  fthsetcestrc  18108  fullsetcestrc  18109  evlfcl  18165  uncfcurf  18182  hofcl  18202  yonedalem3  18223  yonedainv  18224  yonffthlem  18225  yoniso  18228  isdrs2  18249  isposd  18265  pospropd  18268  poslubmo  18352  posglbmo  18353  mgmplusf  18561  ismgmd  18563  issstrmgm  18564  opifismgm  18570  mgmhmpropd  18609  mgmhmf1o  18611  idmgmhm  18612  issubmgm2  18614  rabsubmgmd  18615  resmgmhm  18622  resmgmhm2  18623  resmgmhm2b  18624  mgmhmco  18625  submgmacs  18628  issgrpd  18641  sgrppropd  18642  ismndd  18667  mndpropd  18670  issubmnd  18672  mndinvmod  18675  ismhmd  18697  mhmpropd  18703  idmhm  18706  mhmf1o  18707  issubmd  18717  mndissubm  18718  0mhm  18730  resmhm  18731  resmhm2  18732  resmhm2b  18733  mhmco  18734  submacs  18738  prdspjmhm  18740  pwsdiagmhm  18742  pwsco1mhm  18743  pwsco2mhm  18744  gsumwspan  18757  frmdsssubm  18772  frmdup1  18775  grpsubf  18935  dfgrp3  18955  mhmmnd  18980  mhmfmhm  18981  issubg4  19061  grpissubg  19062  isnsg3  19076  nsgacs  19078  0nsg  19085  nsgid  19086  qus0subgadd  19115  cycsubmcom  19120  isghmd  19141  ghmmhm  19142  idghm  19147  ghmnsgima  19156  ghmnsgpreima  19157  ghmf1  19162  kerf1ghm  19163  ghmf1o  19164  gaid  19215  subgga  19216  gass  19217  gasubg  19218  cntzsgrpcl  19250  cntzsubm  19254  cntrsubgnsg  19259  lactghmga  19321  symgfixf1  19353  odf1  19478  sylow1lem2  19515  sylow2blem2  19537  sylow3lem1  19543  lsmssv  19559  smndlsmidm  19572  pj1eu  19612  efglem  19632  efgtf  19638  efgred  19664  efgredeu  19668  frgpmhm  19681  frgpuptf  19686  frgpuplem  19688  mulgmhm  19743  ghmcmn  19747  invghm  19749  ablnsg  19763  imasabl  19792  cygabl  19807  gsum2d2lem  19889  gsum2d2  19890  gsumcom2  19891  dprd2d2  19962  ablfaclem2  20004  srgfcl  20118  srgcom4lem  20135  srglmhm  20143  srgrmhm  20144  ringcomlem  20201  isrnghm2d  20372  c0mgm  20381  c0mhm  20382  isrhm2d  20409  subrngringnsg  20475  issubrng2  20480  subrngint  20482  issubrg2  20514  subrgint  20517  rnghmsscmap2  20551  rnghmsscmap  20552  rnghmsubcsetclem2  20554  rhmsscmap2  20580  rhmsscmap  20581  rhmsubcsetclem2  20583  rhmsscrnghm  20587  rhmsubcrngclem2  20589  srhmsubc  20602  rhmsubc  20611  fldhmsubc  20707  primefld  20727  abvn0b  20758  suborng  20798  islmodd  20806  lmodscaf  20824  lmodprop2d  20864  islssd  20875  islss4  20902  lssacs  20907  lsspropd  20958  islmhmd  20980  lmhmima  20988  lmhmpreima  20989  reslmhm  20993  lspextmo  20997  lsmcl  21024  pj1lmhm  21041  islbs2  21098  issubrgd  21130  dflidl2rng  21162  rnglidlmmgm  21189  rhmpreimaidl  21221  rngqiprnglin  21246  expmhm  21380  nn0srg  21381  prmirredlem  21416  expghm  21419  mulgghm2  21420  domnchr  21476  znf1o  21495  zntoslem  21500  znfld  21504  cygznlem3  21513  phlipf  21596  dsmmlss  21688  uvcf1  21736  frlmlbs  21741  lindff1  21764  lindfrn  21765  f1lindf  21766  issubassa2  21836  mvrf1  21930  mplsubglem  21943  mplsubrg  21949  mplcoe5lem  21981  mplcoe2  21983  mplind  22012  evlslem2  22021  evlseu  22025  mhplss  22077  ply1sclf1  22210  evls1maplmhm  22299  mamucl  22323  mamuass  22324  mamudi  22325  mamudir  22326  mamuvs1  22327  mamuvs2  22328  matbas2d  22345  mamumat1cl  22361  mamulid  22363  mamurid  22364  mat1mhm  22406  dmatid  22417  dmatsubcl  22420  dmatsgrp  22421  dmatmulcl  22422  dmatsrng  22423  dmatcrng  22424  scmatscmiddistr  22430  scmatscm  22435  scmatsgrp  22441  scmatsrng  22442  scmatcrng  22443  scmatsgrp1  22444  scmatsrng1  22445  scmatf1  22453  scmatmhm  22456  mavmul0g  22475  mdet1  22523  mdetunilem9  22542  mdetuni0  22543  mdetmul  22545  madutpos  22564  smadiadetlem4  22591  1elcpmat  22637  cpmatacl  22638  cpmatmcl  22641  mat2pmatf1  22651  mat2pmatmul  22653  mat2pmat1  22654  mat2pmatlin  22657  m2cpm  22663  m2cpminvid  22675  m2cpminvid2  22677  decpmatmul  22694  pmatcollpw1  22698  monmatcollpw  22701  pmatcollpw  22703  pmatcollpw3lem  22705  pmatcollpwscmatlem2  22712  pm2mpf1  22721  mp2pm2mplem4  22731  pm2mpmhmlem2  22741  chp0mat  22768  chpidmat  22769  tgclb  22892  mretopd  23014  toponmre  23015  iscldtop  23017  ordtbaslem  23110  ordtbas2  23113  cnt0  23268  haust1  23274  cnhaus  23276  isreg2  23299  dishaus  23304  ordthaus  23306  dfconn2  23341  iunconn  23350  clsconn  23352  2ndcomap  23380  dis2ndc  23382  llynlly  23399  restnlly  23404  restlly  23405  islly2  23406  llyidm  23410  nllyidm  23411  hausllycmp  23416  kgentopon  23460  txbas  23489  ptbasin2  23500  ptbasfi  23503  txcnp  23542  txcnmpt  23546  pthaus  23560  tx1stc  23572  xkococnlem  23581  xkococn  23582  cnmpt21  23593  qtoptop2  23621  qtopeu  23638  kqt0lem  23658  isr0  23659  regr1lem2  23662  kqreglem1  23663  kqreglem2  23664  kqnrmlem1  23665  kqnrmlem2  23666  nrmr0reg  23671  reghmph  23715  nrmhmph  23716  txswaphmeo  23727  qtophmeo  23739  fbun  23762  trfbas2  23765  isfil2  23778  infil  23785  trfil2  23809  filssufilg  23833  hausflim  23903  fclsnei  23941  fclsfnflim  23949  flimfnfcls  23950  ptcmplem1  23974  clssubg  24031  tgpconncomp  24035  qustgplem  24043  tsmsfbas  24050  utoptop  24157  iducn  24205  cstucnd  24206  isxmetd  24249  isxmet2d  24250  xmettpos  24272  prdsdsf  24290  prdsmet  24293  ressprdsds  24294  imasdsf1olem  24296  imasf1oxmet  24298  imasf1omet  24299  blfvalps  24306  xmetresbl  24360  metss2  24435  comet  24436  stdbdmet  24439  stdbdmopn  24441  methaus  24443  met2ndci  24445  metustfbas  24480  nrmmetd  24497  subgngp  24558  ngptgp  24559  sranlm  24607  nlmvscnlem1  24609  nlmvscn  24610  nrginvrcn  24615  lssnlm  24624  nghmcn  24668  qtopbaslem  24681  reconn  24752  xmetdcn2  24761  metdscn  24780  metnrm  24786  elcncf1di  24823  cncfcdm  24826  mulc1cncf  24833  cncfco  24835  reparphti  24931  reparphtiOLD  24932  isncvsngpd  25085  tcphcph  25172  ipcnlem1  25180  ipcn  25181  iscfil3  25208  bcthlem5  25263  rrxmet  25343  minveclem3  25364  minveclem7  25370  ovolicc2lem4  25456  dyadmbl  25536  volcn  25542  itg1addlem1  25628  itg1addlem2  25633  itg1addlem4  25635  mbfi1fseqlem1  25651  mbfi1fseqlem3  25653  mbfi1fseqlem4  25654  mbfi1fseqlem5  25655  dvmptfsum  25914  c1liplem1  25936  dvgt0lem2  25943  ftc1a  25979  ply1domn  26064  ply1divmo  26076  fta1b  26112  ig1peu  26115  coeeu  26165  plydivalg  26242  aaliou2b  26284  ulmss  26341  ulmcn  26343  efif1olem4  26489  efsubm  26495  logccv  26607  logbmpt  26733  logbfval  26735  cvxcl  26930  basellem4  27029  fsumdvdscom  27130  musum  27136  mpodvdsmulf1o  27139  fsumdvdsmul  27140  dvdsmulf1o  27141  fsumdvdsmulOLD  27142  dchrelbasd  27185  dchrmulcl  27195  dchrinv  27207  lgsqrlem2  27293  lgsdchr  27301  lgseisenlem2  27322  lgsquadlem1  27326  lgsquadlem2  27327  2sqreulem4  27400  dchrisumlema  27434  dchrisumlem2  27436  chpdifbndlem2  27500  pntpbnd  27534  pntibndlem3  27538  ssltd  27739  oldbday  27852  addsprop  27925  mulscutlem  28076  divsmo  28129  om2noseqf1o  28237  om2noseqiso  28238  axtgcont  28451  tgjustc1  28457  tgjustc2  28458  iscgrglt  28496  ercgrg  28499  idmot  28519  motco  28522  cnvmot  28523  motcgrg  28526  tgisline  28609  tghilberti2  28620  mirreu3  28636  mirmot  28657  ragperp  28699  foot  28704  mideu  28720  midf  28758  lmimot  28780  trgcopyeu  28788  f1otrgds  28851  f1otrg  28853  f1otrge  28854  xmstrkgc  28868  brbtwn2  28887  axlowdimlem15  28938  axcontlem2  28947  axcontlem10  28955  eengtrkg  28968  eengtrkge  28969  numedglnl  29126  usgredgreu  29200  uspgredg2vtxeu  29202  uspgredg2v  29206  usgredg2v  29209  wlkswwlksf1o  29861  wwlksnextinj  29881  clwlkclwwlkf1  29991  clwwlkf1  30030  frcond4  30251  frgrncvvdeqlem8  30287  frgrncvvdeq  30290  frgrwopreglem4  30296  numclwwlk1lem2f1  30338  nrt2irr  30454  grpoinvf  30513  nvmf  30626  vacn  30675  nmcvcn  30676  smcnlem  30678  sspg  30709  ssps  30711  sspmlem  30713  0lno  30771  blocni  30786  ipblnfi  30836  minvecolem7  30864  unopf1o  31897  cnvunop  31899  unoplin  31901  counop  31902  hmopadj2  31922  hmoplin  31923  bralnfn  31929  lnopeq0i  31988  hmops  32001  hmopm  32002  hmopco  32004  lnconi  32014  cnlnadjlem2  32049  adjmul  32073  adjadd  32074  cdjreui  32413  disjxpin  32569  off2  32617  2ndresdju  32625  fnpreimac  32647  suppovss  32656  f1od2  32696  xrofsup  32742  s3f1  32920  ccatf1  32922  swrdf1  32930  odutos  32942  dfmgc2lem  32969  dfmgc2  32970  pwrssmgc  32974  mgcf1o  32977  mndlactf1  33012  mndractf1  33014  abliso  33022  symgcntz  33059  tocyccntz  33118  conjga  33144  archiabllem1  33164  archiabllem2  33168  urpropd  33201  elrgspnlem2  33212  rlocf1  33242  rrgsubm  33252  subrdom  33253  xrge0slmod  33314  nsgmgc  33378  intlidl  33386  idlinsubrg  33397  rhmimaidl  33398  prmidl2  33407  idlmulssprm  33408  isprmidlc  33413  rhmpreimaprmidl  33417  qsidomlem1  33418  qsidomlem2  33419  ssdifidllem  33422  ssdifidlprm  33424  mxidlprm  33436  mxidlirredi  33437  ssmxidllem  33439  rsprprmprmidl  33488  rsprprmprmidlb  33489  rprmirred  33497  rprmirredb  33498  1arithufdlem4  33513  ply1degltdimlem  33613  ply1degltdim  33614  lindsun  33616  fedgmullem1  33620  fedgmullem2  33621  fedgmul  33622  lactlmhm  33625  assalactf1o  33626  minplyirred  33696  constrsdrg  33760  1smat1  33789  submateq  33794  madjusmdetlem3  33814  zart0  33864  pstmxmet  33882  ofcf  34088  ldgenpisys  34151  rossros  34165  inelcarsg  34297  sibfof  34326  sitmf  34338  hgt750lemb  34642  erdszelem4  35176  erdszelem9  35181  erdsze2lem2  35186  cnpconn  35212  pconnconn  35213  txpconn  35214  ptpconn  35215  cvxpconn  35224  cvxsconn  35225  iccllysconn  35232  cvmseu  35258  cvmliftmo  35266  cvmlift2lem5  35289  cvmlift2lem9  35293  mrsubff1  35496  elmrsubrn  35502  mrsubco  35503  msubff1  35538  mvhf1  35541  r1peuqusdeg1  35625  segconeu  35994  fnessref  36340  neibastop1  36342  filnetlem3  36363  onsuct0  36424  weiunlem2  36446  unblimceq0lem  36489  unbdqndv2  36494  knoppndv  36517  irrdiff  37309  uncf  37588  fin2so  37596  lindsadd  37602  poimirlem4  37613  poimirlem13  37622  poimirlem14  37623  poimirlem26  37635  heicant  37644  mblfinlem2  37647  ftc1anc  37690  sdclem1  37732  isbnd3  37773  prdsbnd  37782  ismtycnv  37791  ismtyhmeolem  37793  ismtyres  37797  bfplem1  37811  bfplem2  37812  bfp  37813  rrnmet  37818  ismrer1  37827  iccbnd  37829  grpokerinj  37882  isdrngo2  37947  rngogrphom  37960  rngohomco  37963  rngoisocnv  37970  iscringd  37987  eqvreldisj1  38811  erprt  38861  lfl0f  39057  lkrlss  39083  lshpsmreu  39097  linepsubN  39741  pmapsub  39757  lautcnv  40079  lautco  40086  idltrn  40139  cdleme50f1  40532  cdleme50laut  40536  istendod  40751  dihf11  41256  dih1dimatlem  41318  lcfl7N  41490  lcfrlem9  41539  mapd1o  41637  hdmapf1oN  41854  hgmapf1oN  41892  fmpocos  42217  qsalrel  42223  rediveud  42426  imacrhmcl  42497  evlselv  42570  fsuppind  42573  nacsfix  42695  rmxypairf1o  42895  wepwsolem  43026  dnnumch3  43031  fnwe2  43037  mpaaeu  43134  idomsubgmo  43177  mon1psubm  43183  deg1mhm  43184  isotone1  44032  isotone2  44033  mnringmulrcld  44212  traxext  44962  disjxp1  45058  disjf1  45172  wessf1ornlem  45174  projf1o  45186  sumnnodd  45623  lptioo2  45624  lptioo1  45625  cncfshift  45867  cncfperiod  45872  dvnprodlem1  45939  fourierdlem42  46142  nnfoctbdjlem  46448  isomennd  46524  smflimlem6  46769  fsetsnf1  47048  cfsetsnfsetf1  47055  otiunsndisjX  47275  imasetpreimafvbijlemf1  47400  iccpartgt  47423  icceuelpart  47432  ichnreuop  47468  sprsymrelfolem2  47489  sprsymrelf  47491  prproropf1o  47503  reupr  47518  reuopreuprim  47522  uhgrimprop  47887  isuspgrim0lem  47888  upgrimtrls  47901  gpgprismgr4cycllem11  48090  opmpoismgm  48150  mgmplusgiopALT  48177  2zlidl  48223  rhmsubcALTV  48268  srhmsubcALTV  48308  fldhmsubcALTV  48316  lindslinindsimp1  48441  1arymaptf1  48626  2arymaptf1  48637  eqfnovd  48849  fmpodg  48852  toslat  48965  catprsc  48997  catprsc2  48998  oppcendc  49002  invfn  49014  iinfssclem2  49039  iinfssc  49041  iinfsubc  49042  discsubc  49048  nelsubclem  49051  resccatlem  49057  funchomf  49081  imasubclem2  49089  imaidfu  49094  imasubc  49135  imassc  49137  imasubc3  49140  fthcomf  49141  idfth  49142  cofidfth  49146  upeu2  49156  isnatd  49207  swapfffth  49267  diag1f1  49291  diag2f1  49293  fucoppc  49394  isthincd  49420  isthincd2  49421  oppcthinco  49423  oppcthinendcALT  49425  functhinclem4  49431  functhincfun  49433  thincfth  49436  thincciso  49437  thinccisod  49438  functermc  49492  arweuthinc  49513  arweutermc  49514  diagffth  49522  funcsn  49525  0fucterm  49527