Theorem ralrimivva 3180

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 3178	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  5096  disjxiun  5104  otsndisj  5479  otiunsndisj  5480  swopo  5557  issod  5581  reuop  6266  fcof1  7262  fliftfund  7288  isof1oidb  7299  isof1oopb  7300  soisores  7302  soisoi  7303  isocnv  7305  f1oiso  7326  oveqrspc2v  7414  oprres  7557  caovclg  7581  caovcomg  7584  off  7671  coof  7677  caofidlcan  7691  caofrss  7692  caonncan  7697  dmmpog  8053  fnmpoovd  8066  fmpoco  8074  fsplitfpar  8097  poxp  8107  fvmpocurryd  8250  smo11  8333  smoiso2  8338  omsmo  8622  nnasmo  8627  coflton  8635  qsdisj2  8768  eroprf  8788  dom2lem  8963  omxpenlem  9042  xpf1o  9103  unxpdomlem3  9199  fofinf1o  9283  dffi3  9382  supmo  9403  infmo  9448  inf3lem6  9586  cantnf  9646  rankxplim  9832  fseqenlem1  9977  fodomacn  10009  iunfictbso  10067  cofsmo  10222  infpssrlem5  10260  enfin2i  10274  fin23lem23  10279  fin23lem27  10281  fin23lem28  10293  compssiso  10327  ltordlem  11703  cju  12182  axdc4uzlem  13948  seqcaopr2  14003  seqhomo  14014  wrd2ind  14688  cshf1  14775  s3sndisj  14933  s3iunsndisj  14934  climcn2  15559  addcn2  15560  mulcn2  15562  o1of2  15579  isercolllem1  15631  fsum2dlem  15736  fsumcom2  15740  fprodser  15915  fprod2dlem  15946  fprodcom2  15950  isprm6  16684  crth  16748  eulerthlem2  16752  vdwlem12  16963  cshwsdisj  17069  imasaddfnlem  17491  imasvscafn  17500  mreexexd  17609  iscatd  17634  oppccomfpropd  17688  isofn  17737  sectmon  17744  ssctr  17787  ssceq  17788  catsubcat  17801  issubc3  17811  fullsubc  17812  fullresc  17813  isfuncd  17827  idfucl  17843  cofucl  17850  funcres2b  17859  fulloppc  17886  fthoppc  17887  idffth  17897  cofull  17898  cofth  17899  ressffth  17902  setcmon  18049  setcepi  18050  resssetc  18054  resscatc  18071  catciso  18073  fthestrcsetc  18111  fullestrcsetc  18112  embedsetcestrclem  18118  fthsetcestrc  18126  fullsetcestrc  18127  evlfcl  18183  uncfcurf  18200  hofcl  18220  yonedalem3  18241  yonedainv  18242  yonffthlem  18243  yoniso  18246  isdrs2  18267  isposd  18283  pospropd  18286  poslubmo  18370  posglbmo  18371  mgmplusf  18577  ismgmd  18579  issstrmgm  18580  opifismgm  18586  mgmhmpropd  18625  mgmhmf1o  18627  idmgmhm  18628  issubmgm2  18630  rabsubmgmd  18631  resmgmhm  18638  resmgmhm2  18639  resmgmhm2b  18640  mgmhmco  18641  submgmacs  18644  issgrpd  18657  sgrppropd  18658  ismndd  18683  mndpropd  18686  issubmnd  18688  mndinvmod  18691  ismhmd  18713  mhmpropd  18719  idmhm  18722  mhmf1o  18723  issubmd  18733  mndissubm  18734  0mhm  18746  resmhm  18747  resmhm2  18748  resmhm2b  18749  mhmco  18750  submacs  18754  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  gsumwspan  18773  frmdsssubm  18788  frmdup1  18791  grpsubf  18951  dfgrp3  18971  mhmmnd  18996  mhmfmhm  18997  issubg4  19077  grpissubg  19078  isnsg3  19092  nsgacs  19094  0nsg  19101  nsgid  19102  qus0subgadd  19131  cycsubmcom  19136  isghmd  19157  ghmmhm  19158  idghm  19163  ghmnsgima  19172  ghmnsgpreima  19173  ghmf1  19178  kerf1ghm  19179  ghmf1o  19180  gaid  19231  subgga  19232  gass  19233  gasubg  19234  cntzsgrpcl  19266  cntzsubm  19270  cntrsubgnsg  19275  lactghmga  19335  symgfixf1  19367  odf1  19492  sylow1lem2  19529  sylow2blem2  19551  sylow3lem1  19557  lsmssv  19573  smndlsmidm  19586  pj1eu  19626  efglem  19646  efgtf  19652  efgred  19678  efgredeu  19682  frgpmhm  19695  frgpuptf  19700  frgpuplem  19702  mulgmhm  19757  ghmcmn  19761  invghm  19763  ablnsg  19777  imasabl  19806  cygabl  19821  gsum2d2lem  19903  gsum2d2  19904  gsumcom2  19905  dprd2d2  19976  ablfaclem2  20018  srgfcl  20105  srgcom4lem  20122  srglmhm  20130  srgrmhm  20131  ringcomlem  20188  isrnghm2d  20359  c0mgm  20368  c0mhm  20369  isrhm2d  20396  subrngringnsg  20462  issubrng2  20467  subrngint  20469  issubrg2  20501  subrgint  20504  rnghmsscmap2  20538  rnghmsscmap  20539  rnghmsubcsetclem2  20541  rhmsscmap2  20567  rhmsscmap  20568  rhmsubcsetclem2  20570  rhmsscrnghm  20574  rhmsubcrngclem2  20576  srhmsubc  20589  rhmsubc  20598  fldhmsubc  20694  primefld  20714  abvn0b  20745  islmodd  20772  lmodscaf  20790  lmodprop2d  20830  islssd  20841  islss4  20868  lssacs  20873  lsspropd  20924  islmhmd  20946  lmhmima  20954  lmhmpreima  20955  reslmhm  20959  lspextmo  20963  lsmcl  20990  pj1lmhm  21007  islbs2  21064  issubrgd  21096  dflidl2rng  21128  rnglidlmmgm  21155  rhmpreimaidl  21187  rngqiprnglin  21212  expmhm  21353  nn0srg  21354  prmirredlem  21382  expghm  21385  mulgghm2  21386  domnchr  21442  znf1o  21461  zntoslem  21466  znfld  21470  cygznlem3  21479  phlipf  21561  dsmmlss  21653  uvcf1  21701  frlmlbs  21706  lindff1  21729  lindfrn  21730  f1lindf  21731  issubassa2  21801  mvrf1  21895  mplsubglem  21908  mplsubrg  21914  mplcoe5lem  21946  mplcoe2  21948  mplind  21977  evlslem2  21986  evlseu  21990  mhplss  22042  ply1sclf1  22175  evls1maplmhm  22264  mamucl  22288  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  matbas2d  22310  mamumat1cl  22326  mamulid  22328  mamurid  22329  mat1mhm  22371  dmatid  22382  dmatsubcl  22385  dmatsgrp  22386  dmatmulcl  22387  dmatsrng  22388  dmatcrng  22389  scmatscmiddistr  22395  scmatscm  22400  scmatsgrp  22406  scmatsrng  22407  scmatcrng  22408  scmatsgrp1  22409  scmatsrng1  22410  scmatf1  22418  scmatmhm  22421  mavmul0g  22440  mdet1  22488  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  madutpos  22529  smadiadetlem4  22556  1elcpmat  22602  cpmatacl  22603  cpmatmcl  22606  mat2pmatf1  22616  mat2pmatmul  22618  mat2pmat1  22619  mat2pmatlin  22622  m2cpm  22628  m2cpminvid  22640  m2cpminvid2  22642  decpmatmul  22659  pmatcollpw1  22663  monmatcollpw  22666  pmatcollpw  22668  pmatcollpw3lem  22670  pmatcollpwscmatlem2  22677  pm2mpf1  22686  mp2pm2mplem4  22696  pm2mpmhmlem2  22706  chp0mat  22733  chpidmat  22734  tgclb  22857  mretopd  22979  toponmre  22980  iscldtop  22982  ordtbaslem  23075  ordtbas2  23078  cnt0  23233  haust1  23239  cnhaus  23241  isreg2  23264  dishaus  23269  ordthaus  23271  dfconn2  23306  iunconn  23315  clsconn  23317  2ndcomap  23345  dis2ndc  23347  llynlly  23364  restnlly  23369  restlly  23370  islly2  23371  llyidm  23375  nllyidm  23376  hausllycmp  23381  kgentopon  23425  txbas  23454  ptbasin2  23465  ptbasfi  23468  txcnp  23507  txcnmpt  23511  pthaus  23525  tx1stc  23537  xkococnlem  23546  xkococn  23547  cnmpt21  23558  qtoptop2  23586  qtopeu  23603  kqt0lem  23623  isr0  23624  regr1lem2  23627  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  nrmr0reg  23636  reghmph  23680  nrmhmph  23681  txswaphmeo  23692  qtophmeo  23704  fbun  23727  trfbas2  23730  isfil2  23743  infil  23750  trfil2  23774  filssufilg  23798  hausflim  23868  fclsnei  23906  fclsfnflim  23914  flimfnfcls  23915  ptcmplem1  23939  clssubg  23996  tgpconncomp  24000  qustgplem  24008  tsmsfbas  24015  utoptop  24122  iducn  24170  cstucnd  24171  isxmetd  24214  isxmet2d  24215  xmettpos  24237  prdsdsf  24255  prdsmet  24258  ressprdsds  24259  imasdsf1olem  24261  imasf1oxmet  24263  imasf1omet  24264  blfvalps  24271  xmetresbl  24325  metss2  24400  comet  24401  stdbdmet  24404  stdbdmopn  24406  methaus  24408  met2ndci  24410  metustfbas  24445  nrmmetd  24462  subgngp  24523  ngptgp  24524  sranlm  24572  nlmvscnlem1  24574  nlmvscn  24575  nrginvrcn  24580  lssnlm  24589  nghmcn  24633  qtopbaslem  24646  reconn  24717  xmetdcn2  24726  metdscn  24745  metnrm  24751  elcncf1di  24788  cncfcdm  24791  mulc1cncf  24798  cncfco  24800  reparphti  24896  reparphtiOLD  24897  isncvsngpd  25050  tcphcph  25137  ipcnlem1  25145  ipcn  25146  iscfil3  25173  bcthlem5  25228  rrxmet  25308  minveclem3  25329  minveclem7  25335  ovolicc2lem4  25421  dyadmbl  25501  volcn  25507  itg1addlem1  25593  itg1addlem2  25598  itg1addlem4  25600  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  dvmptfsum  25879  c1liplem1  25901  dvgt0lem2  25908  ftc1a  25944  ply1domn  26029  ply1divmo  26041  fta1b  26077  ig1peu  26080  coeeu  26130  plydivalg  26207  aaliou2b  26249  ulmss  26306  ulmcn  26308  efif1olem4  26454  efsubm  26460  logccv  26572  logbmpt  26698  logbfval  26700  cvxcl  26895  basellem4  26994  fsumdvdscom  27095  musum  27101  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  dchrelbasd  27150  dchrmulcl  27160  dchrinv  27172  lgsqrlem2  27258  lgsdchr  27266  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  2sqreulem4  27365  dchrisumlema  27399  dchrisumlem2  27401  chpdifbndlem2  27465  pntpbnd  27499  pntibndlem3  27503  ssltd  27703  oldbday  27812  addsprop  27883  mulscutlem  28034  divsmo  28087  om2noseqf1o  28195  om2noseqiso  28196  axtgcont  28396  tgjustc1  28402  tgjustc2  28403  iscgrglt  28441  ercgrg  28444  idmot  28464  motco  28467  cnvmot  28468  motcgrg  28471  tgisline  28554  tghilberti2  28565  mirreu3  28581  mirmot  28602  ragperp  28644  foot  28649  mideu  28665  midf  28703  lmimot  28725  trgcopyeu  28733  f1otrgds  28796  f1otrg  28798  f1otrge  28799  xmstrkgc  28813  brbtwn2  28832  axlowdimlem15  28883  axcontlem2  28892  axcontlem10  28900  eengtrkg  28913  eengtrkge  28914  numedglnl  29071  usgredgreu  29145  uspgredg2vtxeu  29147  uspgredg2v  29151  usgredg2v  29154  wlkswwlksf1o  29809  wwlksnextinj  29829  clwlkclwwlkf1  29939  clwwlkf1  29978  frcond4  30199  frgrncvvdeqlem8  30235  frgrncvvdeq  30238  frgrwopreglem4  30244  numclwwlk1lem2f1  30286  nrt2irr  30402  grpoinvf  30461  nvmf  30574  vacn  30623  nmcvcn  30624  smcnlem  30626  sspg  30657  ssps  30659  sspmlem  30661  0lno  30719  blocni  30734  ipblnfi  30784  minvecolem7  30812  unopf1o  31845  cnvunop  31847  unoplin  31849  counop  31850  hmopadj2  31870  hmoplin  31871  bralnfn  31877  lnopeq0i  31936  hmops  31949  hmopm  31950  hmopco  31952  lnconi  31962  cnlnadjlem2  31997  adjmul  32021  adjadd  32022  cdjreui  32361  disjxpin  32517  off2  32565  2ndresdju  32573  fnpreimac  32595  suppovss  32604  f1od2  32644  xrofsup  32690  s3f1  32868  ccatf1  32870  swrdf1  32878  odutos  32894  dfmgc2lem  32921  dfmgc2  32922  pwrssmgc  32926  mgcf1o  32929  mndlactf1  32967  mndractf1  32969  abliso  32977  symgcntz  33042  tocyccntz  33101  conjga  33127  archiabllem1  33147  archiabllem2  33151  urpropd  33183  elrgspnlem2  33194  rlocf1  33224  rrgsubm  33234  subrdom  33235  suborng  33293  xrge0slmod  33319  nsgmgc  33383  intlidl  33391  idlinsubrg  33402  rhmimaidl  33403  prmidl2  33412  idlmulssprm  33413  isprmidlc  33418  rhmpreimaprmidl  33422  qsidomlem1  33423  qsidomlem2  33424  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  ssmxidllem  33444  rsprprmprmidl  33493  rsprprmprmidlb  33494  rprmirred  33502  rprmirredb  33503  1arithufdlem4  33518  ply1degltdimlem  33618  ply1degltdim  33619  lindsun  33621  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  lactlmhm  33630  assalactf1o  33631  minplyirred  33701  constrsdrg  33765  1smat1  33794  submateq  33799  madjusmdetlem3  33819  zart0  33869  pstmxmet  33887  ofcf  34093  ldgenpisys  34156  rossros  34170  inelcarsg  34302  sibfof  34331  sitmf  34343  hgt750lemb  34647  erdszelem4  35181  erdszelem9  35186  erdsze2lem2  35191  cnpconn  35217  pconnconn  35218  txpconn  35219  ptpconn  35220  cvxpconn  35229  cvxsconn  35230  iccllysconn  35237  cvmseu  35263  cvmliftmo  35271  cvmlift2lem5  35294  cvmlift2lem9  35298  mrsubff1  35501  elmrsubrn  35507  mrsubco  35508  msubff1  35543  mvhf1  35546  r1peuqusdeg1  35630  segconeu  35999  fnessref  36345  neibastop1  36347  filnetlem3  36368  onsuct0  36429  weiunlem2  36451  unblimceq0lem  36494  unbdqndv2  36499  knoppndv  36522  irrdiff  37314  uncf  37593  fin2so  37601  lindsadd  37607  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  poimirlem26  37640  heicant  37649  mblfinlem2  37652  ftc1anc  37695  sdclem1  37737  isbnd3  37778  prdsbnd  37787  ismtycnv  37796  ismtyhmeolem  37798  ismtyres  37802  bfplem1  37816  bfplem2  37817  bfp  37818  rrnmet  37823  ismrer1  37832  iccbnd  37834  grpokerinj  37887  isdrngo2  37952  rngogrphom  37965  rngohomco  37968  rngoisocnv  37975  iscringd  37992  eqvreldisj1  38816  erprt  38866  lfl0f  39062  lkrlss  39088  lshpsmreu  39102  linepsubN  39746  pmapsub  39762  lautcnv  40084  lautco  40091  idltrn  40144  cdleme50f1  40537  cdleme50laut  40541  istendod  40756  dihf11  41261  dih1dimatlem  41323  lcfl7N  41495  lcfrlem9  41544  mapd1o  41642  hdmapf1oN  41859  hgmapf1oN  41897  fmpocos  42222  qsalrel  42228  rediveud  42431  imacrhmcl  42502  evlselv  42575  fsuppind  42578  nacsfix  42700  rmxypairf1o  42900  wepwsolem  43031  dnnumch3  43036  fnwe2  43042  mpaaeu  43139  idomsubgmo  43182  mon1psubm  43188  deg1mhm  43189  isotone1  44037  isotone2  44038  mnringmulrcld  44217  traxext  44967  disjxp1  45063  disjf1  45177  wessf1ornlem  45179  projf1o  45191  sumnnodd  45628  lptioo2  45629  lptioo1  45630  cncfshift  45872  cncfperiod  45877  dvnprodlem1  45944  fourierdlem42  46147  nnfoctbdjlem  46453  isomennd  46529  smflimlem6  46774  fsetsnf1  47053  cfsetsnfsetf1  47060  otiunsndisjX  47280  imasetpreimafvbijlemf1  47405  iccpartgt  47428  icceuelpart  47437  ichnreuop  47473  sprsymrelfolem2  47494  sprsymrelf  47496  prproropf1o  47508  reupr  47523  reuopreuprim  47527  uhgrimprop  47892  isuspgrim0lem  47893  upgrimtrls  47906  gpgprismgr4cycllem11  48095  opmpoismgm  48155  mgmplusgiopALT  48182  2zlidl  48228  rhmsubcALTV  48273  srhmsubcALTV  48313  fldhmsubcALTV  48321  lindslinindsimp1  48446  1arymaptf1  48631  2arymaptf1  48642  eqfnovd  48854  fmpodg  48857  toslat  48970  catprsc  49002  catprsc2  49003  oppcendc  49007  invfn  49019  iinfssclem2  49044  iinfssc  49046  iinfsubc  49047  discsubc  49053  nelsubclem  49056  resccatlem  49062  funchomf  49086  imasubclem2  49094  imaidfu  49099  imasubc  49140  imassc  49142  imasubc3  49145  fthcomf  49146  idfth  49147  cofidfth  49151  upeu2  49161  isnatd  49212  swapfffth  49272  diag1f1  49296  diag2f1  49298  fucoppc  49399  isthincd  49425  isthincd2  49426  oppcthinco  49428  oppcthinendcALT  49430  functhinclem4  49436  functhincfun  49438  thincfth  49441  thincciso  49442  thinccisod  49443  functermc  49497  arweuthinc  49518  arweutermc  49519  diagffth  49527  funcsn  49530  0fucterm  49532