Theorem ralrimivva 3172

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 3170	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  5081  disjxiun  5089  otsndisj  5462  otiunsndisj  5463  swopo  5538  issod  5562  reuop  6241  fcof1  7224  fliftfund  7250  isof1oidb  7261  isof1oopb  7262  soisores  7264  soisoi  7265  isocnv  7267  f1oiso  7288  oveqrspc2v  7376  oprres  7517  caovclg  7541  caovcomg  7544  off  7631  coof  7637  caofidlcan  7651  caofrss  7652  caonncan  7657  dmmpog  8009  fnmpoovd  8020  fmpoco  8028  fsplitfpar  8051  poxp  8061  fvmpocurryd  8204  smo11  8287  smoiso2  8292  omsmo  8576  nnasmo  8581  coflton  8589  qsdisj2  8722  eroprf  8742  dom2lem  8917  omxpenlem  8995  xpf1o  9056  unxpdomlem3  9147  fofinf1o  9222  dffi3  9321  supmo  9342  infmo  9387  inf3lem6  9529  cantnf  9589  rankxplim  9775  fseqenlem1  9918  fodomacn  9950  iunfictbso  10008  cofsmo  10163  infpssrlem5  10201  enfin2i  10215  fin23lem23  10220  fin23lem27  10222  fin23lem28  10234  compssiso  10268  ltordlem  11645  cju  12124  axdc4uzlem  13890  seqcaopr2  13945  seqhomo  13956  wrd2ind  14629  cshf1  14716  s3sndisj  14874  s3iunsndisj  14875  climcn2  15500  addcn2  15501  mulcn2  15503  o1of2  15520  isercolllem1  15572  fsum2dlem  15677  fsumcom2  15681  fprodser  15856  fprod2dlem  15887  fprodcom2  15891  isprm6  16625  crth  16689  eulerthlem2  16693  vdwlem12  16904  cshwsdisj  17010  imasaddfnlem  17432  imasvscafn  17441  mreexexd  17554  iscatd  17579  oppccomfpropd  17633  isofn  17682  sectmon  17689  ssctr  17732  ssceq  17733  catsubcat  17746  issubc3  17756  fullsubc  17757  fullresc  17758  isfuncd  17772  idfucl  17788  cofucl  17795  funcres2b  17804  fulloppc  17831  fthoppc  17832  idffth  17842  cofull  17843  cofth  17844  ressffth  17847  setcmon  17994  setcepi  17995  resssetc  17999  resscatc  18016  catciso  18018  fthestrcsetc  18056  fullestrcsetc  18057  embedsetcestrclem  18063  fthsetcestrc  18071  fullsetcestrc  18072  evlfcl  18128  uncfcurf  18145  hofcl  18165  yonedalem3  18186  yonedainv  18187  yonffthlem  18188  yoniso  18191  isdrs2  18212  isposd  18228  pospropd  18231  poslubmo  18315  posglbmo  18316  mgmplusf  18524  ismgmd  18526  issstrmgm  18527  opifismgm  18533  mgmhmpropd  18572  mgmhmf1o  18574  idmgmhm  18575  issubmgm2  18577  rabsubmgmd  18578  resmgmhm  18585  resmgmhm2  18586  resmgmhm2b  18587  mgmhmco  18588  submgmacs  18591  issgrpd  18604  sgrppropd  18605  ismndd  18630  mndpropd  18633  issubmnd  18635  mndinvmod  18638  ismhmd  18660  mhmpropd  18666  idmhm  18669  mhmf1o  18670  issubmd  18680  mndissubm  18681  0mhm  18693  resmhm  18694  resmhm2  18695  resmhm2b  18696  mhmco  18697  submacs  18701  prdspjmhm  18703  pwsdiagmhm  18705  pwsco1mhm  18706  pwsco2mhm  18707  gsumwspan  18720  frmdsssubm  18735  frmdup1  18738  grpsubf  18898  dfgrp3  18918  mhmmnd  18943  mhmfmhm  18944  issubg4  19024  grpissubg  19025  isnsg3  19039  nsgacs  19041  0nsg  19048  nsgid  19049  qus0subgadd  19078  cycsubmcom  19083  isghmd  19104  ghmmhm  19105  idghm  19110  ghmnsgima  19119  ghmnsgpreima  19120  ghmf1  19125  kerf1ghm  19126  ghmf1o  19127  gaid  19178  subgga  19179  gass  19180  gasubg  19181  cntzsgrpcl  19213  cntzsubm  19217  cntrsubgnsg  19222  lactghmga  19284  symgfixf1  19316  odf1  19441  sylow1lem2  19478  sylow2blem2  19500  sylow3lem1  19506  lsmssv  19522  smndlsmidm  19535  pj1eu  19575  efglem  19595  efgtf  19601  efgred  19627  efgredeu  19631  frgpmhm  19644  frgpuptf  19649  frgpuplem  19651  mulgmhm  19706  ghmcmn  19710  invghm  19712  ablnsg  19726  imasabl  19755  cygabl  19770  gsum2d2lem  19852  gsum2d2  19853  gsumcom2  19854  dprd2d2  19925  ablfaclem2  19967  srgfcl  20081  srgcom4lem  20098  srglmhm  20106  srgrmhm  20107  ringcomlem  20164  isrnghm2d  20335  c0mgm  20344  c0mhm  20345  isrhm2d  20372  subrngringnsg  20438  issubrng2  20443  subrngint  20445  issubrg2  20477  subrgint  20480  rnghmsscmap2  20514  rnghmsscmap  20515  rnghmsubcsetclem2  20517  rhmsscmap2  20543  rhmsscmap  20544  rhmsubcsetclem2  20546  rhmsscrnghm  20550  rhmsubcrngclem2  20552  srhmsubc  20565  rhmsubc  20574  fldhmsubc  20670  primefld  20690  abvn0b  20721  suborng  20761  islmodd  20769  lmodscaf  20787  lmodprop2d  20827  islssd  20838  islss4  20865  lssacs  20870  lsspropd  20921  islmhmd  20943  lmhmima  20951  lmhmpreima  20952  reslmhm  20956  lspextmo  20960  lsmcl  20987  pj1lmhm  21004  islbs2  21061  issubrgd  21093  dflidl2rng  21125  rnglidlmmgm  21152  rhmpreimaidl  21184  rngqiprnglin  21209  expmhm  21343  nn0srg  21344  prmirredlem  21379  expghm  21382  mulgghm2  21383  domnchr  21439  znf1o  21458  zntoslem  21463  znfld  21467  cygznlem3  21476  phlipf  21559  dsmmlss  21651  uvcf1  21699  frlmlbs  21704  lindff1  21727  lindfrn  21728  f1lindf  21729  issubassa2  21799  mvrf1  21893  mplsubglem  21906  mplsubrg  21912  mplcoe5lem  21944  mplcoe2  21946  mplind  21975  evlslem2  21984  evlseu  21988  mhplss  22040  ply1sclf1  22173  evls1maplmhm  22262  mamucl  22286  mamuass  22287  mamudi  22288  mamudir  22289  mamuvs1  22290  mamuvs2  22291  matbas2d  22308  mamumat1cl  22324  mamulid  22326  mamurid  22327  mat1mhm  22369  dmatid  22380  dmatsubcl  22383  dmatsgrp  22384  dmatmulcl  22385  dmatsrng  22386  dmatcrng  22387  scmatscmiddistr  22393  scmatscm  22398  scmatsgrp  22404  scmatsrng  22405  scmatcrng  22406  scmatsgrp1  22407  scmatsrng1  22408  scmatf1  22416  scmatmhm  22419  mavmul0g  22438  mdet1  22486  mdetunilem9  22505  mdetuni0  22506  mdetmul  22508  madutpos  22527  smadiadetlem4  22554  1elcpmat  22600  cpmatacl  22601  cpmatmcl  22604  mat2pmatf1  22614  mat2pmatmul  22616  mat2pmat1  22617  mat2pmatlin  22620  m2cpm  22626  m2cpminvid  22638  m2cpminvid2  22640  decpmatmul  22657  pmatcollpw1  22661  monmatcollpw  22664  pmatcollpw  22666  pmatcollpw3lem  22668  pmatcollpwscmatlem2  22675  pm2mpf1  22684  mp2pm2mplem4  22694  pm2mpmhmlem2  22704  chp0mat  22731  chpidmat  22732  tgclb  22855  mretopd  22977  toponmre  22978  iscldtop  22980  ordtbaslem  23073  ordtbas2  23076  cnt0  23231  haust1  23237  cnhaus  23239  isreg2  23262  dishaus  23267  ordthaus  23269  dfconn2  23304  iunconn  23313  clsconn  23315  2ndcomap  23343  dis2ndc  23345  llynlly  23362  restnlly  23367  restlly  23368  islly2  23369  llyidm  23373  nllyidm  23374  hausllycmp  23379  kgentopon  23423  txbas  23452  ptbasin2  23463  ptbasfi  23466  txcnp  23505  txcnmpt  23509  pthaus  23523  tx1stc  23535  xkococnlem  23544  xkococn  23545  cnmpt21  23556  qtoptop2  23584  qtopeu  23601  kqt0lem  23621  isr0  23622  regr1lem2  23625  kqreglem1  23626  kqreglem2  23627  kqnrmlem1  23628  kqnrmlem2  23629  nrmr0reg  23634  reghmph  23678  nrmhmph  23679  txswaphmeo  23690  qtophmeo  23702  fbun  23725  trfbas2  23728  isfil2  23741  infil  23748  trfil2  23772  filssufilg  23796  hausflim  23866  fclsnei  23904  fclsfnflim  23912  flimfnfcls  23913  ptcmplem1  23937  clssubg  23994  tgpconncomp  23998  qustgplem  24006  tsmsfbas  24013  utoptop  24120  iducn  24168  cstucnd  24169  isxmetd  24212  isxmet2d  24213  xmettpos  24235  prdsdsf  24253  prdsmet  24256  ressprdsds  24257  imasdsf1olem  24259  imasf1oxmet  24261  imasf1omet  24262  blfvalps  24269  xmetresbl  24323  metss2  24398  comet  24399  stdbdmet  24402  stdbdmopn  24404  methaus  24406  met2ndci  24408  metustfbas  24443  nrmmetd  24460  subgngp  24521  ngptgp  24522  sranlm  24570  nlmvscnlem1  24572  nlmvscn  24573  nrginvrcn  24578  lssnlm  24587  nghmcn  24631  qtopbaslem  24644  reconn  24715  xmetdcn2  24724  metdscn  24743  metnrm  24749  elcncf1di  24786  cncfcdm  24789  mulc1cncf  24796  cncfco  24798  reparphti  24894  reparphtiOLD  24895  isncvsngpd  25048  tcphcph  25135  ipcnlem1  25143  ipcn  25144  iscfil3  25171  bcthlem5  25226  rrxmet  25306  minveclem3  25327  minveclem7  25333  ovolicc2lem4  25419  dyadmbl  25499  volcn  25505  itg1addlem1  25591  itg1addlem2  25596  itg1addlem4  25598  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  dvmptfsum  25877  c1liplem1  25899  dvgt0lem2  25906  ftc1a  25942  ply1domn  26027  ply1divmo  26039  fta1b  26075  ig1peu  26078  coeeu  26128  plydivalg  26205  aaliou2b  26247  ulmss  26304  ulmcn  26306  efif1olem4  26452  efsubm  26458  logccv  26570  logbmpt  26696  logbfval  26698  cvxcl  26893  basellem4  26992  fsumdvdscom  27093  musum  27099  mpodvdsmulf1o  27102  fsumdvdsmul  27103  dvdsmulf1o  27104  fsumdvdsmulOLD  27105  dchrelbasd  27148  dchrmulcl  27158  dchrinv  27170  lgsqrlem2  27256  lgsdchr  27264  lgseisenlem2  27285  lgsquadlem1  27289  lgsquadlem2  27290  2sqreulem4  27363  dchrisumlema  27397  dchrisumlem2  27399  chpdifbndlem2  27463  pntpbnd  27497  pntibndlem3  27501  ssltd  27702  oldbday  27817  addsprop  27890  mulscutlem  28041  divsmo  28094  om2noseqf1o  28202  om2noseqiso  28203  axtgcont  28418  tgjustc1  28424  tgjustc2  28425  iscgrglt  28463  ercgrg  28466  idmot  28486  motco  28489  cnvmot  28490  motcgrg  28493  tgisline  28576  tghilberti2  28587  mirreu3  28603  mirmot  28624  ragperp  28666  foot  28671  mideu  28687  midf  28725  lmimot  28747  trgcopyeu  28755  f1otrgds  28818  f1otrg  28820  f1otrge  28821  xmstrkgc  28835  brbtwn2  28854  axlowdimlem15  28905  axcontlem2  28914  axcontlem10  28922  eengtrkg  28935  eengtrkge  28936  numedglnl  29093  usgredgreu  29167  uspgredg2vtxeu  29169  uspgredg2v  29173  usgredg2v  29176  wlkswwlksf1o  29828  wwlksnextinj  29848  clwlkclwwlkf1  29958  clwwlkf1  29997  frcond4  30218  frgrncvvdeqlem8  30254  frgrncvvdeq  30257  frgrwopreglem4  30263  numclwwlk1lem2f1  30305  nrt2irr  30421  grpoinvf  30480  nvmf  30593  vacn  30642  nmcvcn  30643  smcnlem  30645  sspg  30676  ssps  30678  sspmlem  30680  0lno  30738  blocni  30753  ipblnfi  30803  minvecolem7  30831  unopf1o  31864  cnvunop  31866  unoplin  31868  counop  31869  hmopadj2  31889  hmoplin  31890  bralnfn  31896  lnopeq0i  31955  hmops  31968  hmopm  31969  hmopco  31971  lnconi  31981  cnlnadjlem2  32016  adjmul  32040  adjadd  32041  cdjreui  32380  disjxpin  32537  off2  32592  2ndresdju  32600  fnpreimac  32622  suppovss  32631  f1od2  32671  xrofsup  32719  s3f1  32897  ccatf1  32899  swrdf1  32907  odutos  32919  dfmgc2lem  32946  dfmgc2  32947  pwrssmgc  32951  mgcf1o  32954  mndlactf1  32989  mndractf1  32991  abliso  32999  symgcntz  33036  tocyccntz  33095  conjga  33121  fxpsubrg  33125  archiabllem1  33144  archiabllem2  33148  urpropd  33181  elrgspnlem2  33192  rlocf1  33222  rrgsubm  33232  subrdom  33233  xrge0slmod  33294  nsgmgc  33358  intlidl  33366  idlinsubrg  33377  rhmimaidl  33378  prmidl2  33387  idlmulssprm  33388  isprmidlc  33393  rhmpreimaprmidl  33397  qsidomlem1  33398  qsidomlem2  33399  ssdifidllem  33402  ssdifidlprm  33404  mxidlprm  33416  mxidlirredi  33417  ssmxidllem  33419  rsprprmprmidl  33468  rsprprmprmidlb  33469  rprmirred  33477  rprmirredb  33478  1arithufdlem4  33493  mplvrpmga  33556  ply1degltdimlem  33605  ply1degltdim  33606  lindsun  33608  fedgmullem1  33612  fedgmullem2  33613  fedgmul  33614  lactlmhm  33617  assalactf1o  33618  minplyirred  33694  constrsdrg  33758  1smat1  33787  submateq  33792  madjusmdetlem3  33812  zart0  33862  pstmxmet  33880  ofcf  34086  ldgenpisys  34149  rossros  34163  inelcarsg  34295  sibfof  34324  sitmf  34336  hgt750lemb  34640  erdszelem4  35187  erdszelem9  35192  erdsze2lem2  35197  cnpconn  35223  pconnconn  35224  txpconn  35225  ptpconn  35226  cvxpconn  35235  cvxsconn  35236  iccllysconn  35243  cvmseu  35269  cvmliftmo  35277  cvmlift2lem5  35300  cvmlift2lem9  35304  mrsubff1  35507  elmrsubrn  35513  mrsubco  35514  msubff1  35549  mvhf1  35552  r1peuqusdeg1  35636  segconeu  36005  fnessref  36351  neibastop1  36353  filnetlem3  36374  onsuct0  36435  weiunlem2  36457  unblimceq0lem  36500  unbdqndv2  36505  knoppndv  36528  irrdiff  37320  uncf  37599  fin2so  37607  lindsadd  37613  poimirlem4  37624  poimirlem13  37633  poimirlem14  37634  poimirlem26  37646  heicant  37655  mblfinlem2  37658  ftc1anc  37701  sdclem1  37743  isbnd3  37784  prdsbnd  37793  ismtycnv  37802  ismtyhmeolem  37804  ismtyres  37808  bfplem1  37822  bfplem2  37823  bfp  37824  rrnmet  37829  ismrer1  37838  iccbnd  37840  grpokerinj  37893  isdrngo2  37958  rngogrphom  37971  rngohomco  37974  rngoisocnv  37981  iscringd  37998  eqvreldisj1  38822  erprt  38872  lfl0f  39068  lkrlss  39094  lshpsmreu  39108  linepsubN  39751  pmapsub  39767  lautcnv  40089  lautco  40096  idltrn  40149  cdleme50f1  40542  cdleme50laut  40546  istendod  40761  dihf11  41266  dih1dimatlem  41328  lcfl7N  41500  lcfrlem9  41549  mapd1o  41647  hdmapf1oN  41864  hgmapf1oN  41902  fmpocos  42227  qsalrel  42233  rediveud  42436  imacrhmcl  42507  evlselv  42580  fsuppind  42583  nacsfix  42705  rmxypairf1o  42904  wepwsolem  43035  dnnumch3  43040  fnwe2  43046  mpaaeu  43143  idomsubgmo  43186  mon1psubm  43192  deg1mhm  43193  isotone1  44041  isotone2  44042  mnringmulrcld  44221  traxext  44971  disjxp1  45067  disjf1  45181  wessf1ornlem  45183  projf1o  45195  sumnnodd  45631  lptioo2  45632  lptioo1  45633  cncfshift  45875  cncfperiod  45880  dvnprodlem1  45947  fourierdlem42  46150  nnfoctbdjlem  46456  isomennd  46532  smflimlem6  46777  fsetsnf1  47056  cfsetsnfsetf1  47063  otiunsndisjX  47283  imasetpreimafvbijlemf1  47408  iccpartgt  47431  icceuelpart  47440  ichnreuop  47476  sprsymrelfolem2  47497  sprsymrelf  47499  prproropf1o  47511  reupr  47526  reuopreuprim  47530  uhgrimprop  47896  isuspgrim0lem  47897  upgrimtrls  47910  gpgprismgr4cycllem11  48109  opmpoismgm  48171  mgmplusgiopALT  48198  2zlidl  48244  rhmsubcALTV  48289  srhmsubcALTV  48329  fldhmsubcALTV  48337  lindslinindsimp1  48462  1arymaptf1  48647  2arymaptf1  48658  eqfnovd  48870  fmpodg  48873  toslat  48986  catprsc  49018  catprsc2  49019  oppcendc  49023  invfn  49035  iinfssclem2  49060  iinfssc  49062  iinfsubc  49063  discsubc  49069  nelsubclem  49072  resccatlem  49078  funchomf  49102  imasubclem2  49110  imaidfu  49115  imasubc  49156  imassc  49158  imasubc3  49161  fthcomf  49162  idfth  49163  cofidfth  49167  upeu2  49177  isnatd  49228  swapfffth  49288  diag1f1  49312  diag2f1  49314  fucoppc  49415  isthincd  49441  isthincd2  49442  oppcthinco  49444  oppcthinendcALT  49446  functhinclem4  49452  functhincfun  49454  thincfth  49457  thincciso  49458  thinccisod  49459  functermc  49513  arweuthinc  49534  arweutermc  49535  diagffth  49543  funcsn  49546  0fucterm  49548