Theorem ralrimivva 3198

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  disjord  5135  disjxiun  5144  otsndisj  5518  otiunsndisj  5519  swopo  5598  issod  5620  reuop  6291  fcof1  7287  fliftfund  7312  isof1oidb  7323  isof1oopb  7324  soisores  7326  soisoi  7327  isocnv  7329  f1oiso  7350  oveqrspc2v  7438  oprres  7577  caovclg  7601  caovcomg  7604  off  7690  caofrss  7708  caonncan  7713  dmmpog  8063  fnmpoovd  8075  fmpoco  8083  fsplitfpar  8106  poxp  8116  fvmpocurryd  8258  smo11  8366  smoiso2  8371  omsmo  8659  nnasmo  8664  coflton  8672  qsdisj2  8791  eroprf  8811  dom2lem  8990  omxpenlem  9075  xpf1o  9141  unxpdomlem3  9254  fofinf1o  9329  dffi3  9428  supmo  9449  infmo  9492  inf3lem6  9630  cantnf  9690  rankxplim  9876  fseqenlem1  10021  fodomacn  10053  iunfictbso  10111  cofsmo  10266  infpssrlem5  10304  enfin2i  10318  fin23lem23  10323  fin23lem27  10325  fin23lem28  10337  compssiso  10371  ltordlem  11743  cju  12212  axdc4uzlem  13952  seqcaopr2  14008  seqhomo  14019  wrd2ind  14677  cshf1  14764  s3sndisj  14918  s3iunsndisj  14919  climcn2  15541  addcn2  15542  mulcn2  15544  o1of2  15561  isercolllem1  15615  fsum2dlem  15720  fsumcom2  15724  fprodser  15897  fprod2dlem  15928  fprodcom2  15932  isprm6  16655  crth  16715  eulerthlem2  16719  vdwlem12  16929  cshwsdisj  17036  imasaddfnlem  17478  imasvscafn  17487  mreexexd  17596  iscatd  17621  oppccomfpropd  17677  isofn  17726  sectmon  17733  ssctr  17776  ssceq  17777  catsubcat  17793  issubc3  17803  fullsubc  17804  fullresc  17805  isfuncd  17819  idfucl  17835  cofucl  17842  funcres2b  17851  fulloppc  17877  fthoppc  17878  idffth  17888  cofull  17889  cofth  17890  ressffth  17893  setcmon  18041  setcepi  18042  resssetc  18046  resscatc  18063  catciso  18065  fthestrcsetc  18106  fullestrcsetc  18107  embedsetcestrclem  18113  fthsetcestrc  18121  fullsetcestrc  18122  evlfcl  18179  uncfcurf  18196  hofcl  18216  yonedalem3  18237  yonedainv  18238  yonffthlem  18239  yoniso  18242  isdrs2  18263  isposd  18280  pospropd  18284  poslubmo  18368  posglbmo  18369  mgmplusf  18575  ismgmd  18577  issstrmgm  18578  opifismgm  18584  mgmhmpropd  18623  mgmhmf1o  18625  idmgmhm  18626  issubmgm2  18628  rabsubmgmd  18629  resmgmhm  18636  resmgmhm2  18637  resmgmhm2b  18638  mgmhmco  18639  submgmacs  18642  issgrpd  18655  sgrppropd  18656  ismndd  18681  mndpropd  18684  issubmnd  18686  mndinvmod  18689  ismhmd  18708  mhmpropd  18714  idmhm  18717  mhmf1o  18718  issubmd  18723  mndissubm  18724  0mhm  18736  resmhm  18737  resmhm2  18738  resmhm2b  18739  mhmco  18740  submacs  18744  prdspjmhm  18746  pwsdiagmhm  18748  pwsco1mhm  18749  pwsco2mhm  18750  gsumwspan  18763  frmdsssubm  18778  frmdup1  18781  grpsubf  18938  dfgrp3  18958  mhmmnd  18983  mhmfmhm  18984  issubg4  19061  grpissubg  19062  isnsg3  19076  nsgacs  19078  0nsg  19085  nsgid  19086  qus0subgadd  19114  cycsubmcom  19119  isghmd  19139  ghmmhm  19140  idghm  19145  ghmnsgima  19154  ghmnsgpreima  19155  ghmf1  19160  kerf1ghm  19161  ghmf1o  19162  gaid  19204  subgga  19205  gass  19206  gasubg  19207  cntzsgrpcl  19239  cntzsubm  19243  cntrsubgnsg  19248  lactghmga  19314  symgfixf1  19346  odf1  19471  sylow1lem2  19508  sylow2blem2  19530  sylow3lem1  19536  lsmssv  19552  smndlsmidm  19565  pj1eu  19605  efglem  19625  efgtf  19631  efgred  19657  efgredeu  19661  frgpmhm  19674  frgpuptf  19679  frgpuplem  19681  mulgmhm  19736  ghmcmn  19740  invghm  19742  ablnsg  19756  imasabl  19785  cygabl  19800  gsum2d2lem  19882  gsum2d2  19883  gsumcom2  19884  dprd2d2  19955  ablfaclem2  19997  srgfcl  20090  srgcom4lem  20107  srglmhm  20115  srgrmhm  20116  ringcomlem  20167  isrnghm2d  20341  c0mgm  20350  c0mhm  20351  isrhm2d  20378  subrngringnsg  20441  issubrng2  20446  subrngint  20448  issubrg2  20482  subrgint  20485  primefld  20564  islmodd  20620  lmodscaf  20638  lmodprop2d  20678  islssd  20690  islss4  20717  lssacs  20722  lsspropd  20772  islmhmd  20794  lmhmima  20802  lmhmpreima  20803  reslmhm  20807  lspextmo  20811  lsmcl  20838  pj1lmhm  20855  islbs2  20912  issubrgd  20956  dflidl2  20992  dflidl2rng  21030  rnglidlmmgm  21034  rngqiprnglin  21061  opprdomn  21119  abvn0b  21120  expmhm  21214  nn0srg  21215  prmirredlem  21243  expghm  21246  mulgghm2  21247  domnchr  21303  znf1o  21326  zntoslem  21331  znfld  21335  cygznlem3  21344  phlipf  21424  dsmmlss  21518  uvcf1  21566  frlmlbs  21571  lindff1  21594  lindfrn  21595  f1lindf  21596  issubassa2  21665  mvrf1  21764  mplsubglem  21777  mplsubrg  21783  mplcoe5lem  21813  mplcoe2  21815  mplind  21850  evlslem2  21861  evlseu  21865  mhplss  21917  ply1sclf1  22031  mamucl  22121  mamuass  22122  mamudi  22123  mamudir  22124  mamuvs1  22125  mamuvs2  22126  matbas2d  22145  mamumat1cl  22161  mamulid  22163  mamurid  22164  mat1mhm  22206  dmatid  22217  dmatsubcl  22220  dmatsgrp  22221  dmatmulcl  22222  dmatsrng  22223  dmatcrng  22224  scmatscmiddistr  22230  scmatscm  22235  scmatsgrp  22241  scmatsrng  22242  scmatcrng  22243  scmatsgrp1  22244  scmatsrng1  22245  scmatf1  22253  scmatmhm  22256  mavmul0g  22275  mdet1  22323  mdetunilem9  22342  mdetuni0  22343  mdetmul  22345  madutpos  22364  smadiadetlem4  22391  1elcpmat  22437  cpmatacl  22438  cpmatmcl  22441  mat2pmatf1  22451  mat2pmatmul  22453  mat2pmat1  22454  mat2pmatlin  22457  m2cpm  22463  m2cpminvid  22475  m2cpminvid2  22477  decpmatmul  22494  pmatcollpw1  22498  monmatcollpw  22501  pmatcollpw  22503  pmatcollpw3lem  22505  pmatcollpwscmatlem2  22512  pm2mpf1  22521  mp2pm2mplem4  22531  pm2mpmhmlem2  22541  chp0mat  22568  chpidmat  22569  tgclb  22693  mretopd  22816  toponmre  22817  iscldtop  22819  ordtbaslem  22912  ordtbas2  22915  cnt0  23070  haust1  23076  cnhaus  23078  isreg2  23101  dishaus  23106  ordthaus  23108  dfconn2  23143  iunconn  23152  clsconn  23154  2ndcomap  23182  dis2ndc  23184  llynlly  23201  restnlly  23206  restlly  23207  islly2  23208  llyidm  23212  nllyidm  23213  hausllycmp  23218  kgentopon  23262  txbas  23291  ptbasin2  23302  ptbasfi  23305  txcnp  23344  txcnmpt  23348  pthaus  23362  tx1stc  23374  xkococnlem  23383  xkococn  23384  cnmpt21  23395  qtoptop2  23423  qtopeu  23440  kqt0lem  23460  isr0  23461  regr1lem2  23464  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  nrmr0reg  23473  reghmph  23517  nrmhmph  23518  txswaphmeo  23529  qtophmeo  23541  fbun  23564  trfbas2  23567  isfil2  23580  infil  23587  trfil2  23611  filssufilg  23635  hausflim  23705  fclsnei  23743  fclsfnflim  23751  flimfnfcls  23752  ptcmplem1  23776  clssubg  23833  tgpconncomp  23837  qustgplem  23845  tsmsfbas  23852  utoptop  23959  iducn  24008  cstucnd  24009  isxmetd  24052  isxmet2d  24053  xmettpos  24075  prdsdsf  24093  prdsmet  24096  ressprdsds  24097  imasdsf1olem  24099  imasf1oxmet  24101  imasf1omet  24102  blfvalps  24109  xmetresbl  24163  metss2  24241  comet  24242  stdbdmet  24245  stdbdmopn  24247  methaus  24249  met2ndci  24251  metustfbas  24286  nrmmetd  24303  subgngp  24364  ngptgp  24365  sranlm  24421  nlmvscnlem1  24423  nlmvscn  24424  nrginvrcn  24429  lssnlm  24438  nghmcn  24482  qtopbaslem  24495  reconn  24564  xmetdcn2  24573  metdscn  24592  metnrm  24598  elcncf1di  24635  cncfcdm  24638  mulc1cncf  24645  cncfco  24647  reparphti  24743  reparphtiOLD  24744  isncvsngpd  24898  tcphcph  24985  ipcnlem1  24993  ipcn  24994  iscfil3  25021  bcthlem5  25076  rrxmet  25156  minveclem3  25177  minveclem7  25183  ovolicc2lem4  25269  dyadmbl  25349  volcn  25355  itg1addlem1  25441  itg1addlem2  25446  itg1addlem4  25448  itg1addlem4OLD  25449  mbfi1fseqlem1  25465  mbfi1fseqlem3  25467  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  dvmptfsum  25727  c1liplem1  25748  dvgt0lem2  25755  ftc1a  25789  ply1domn  25876  ply1divmo  25888  fta1b  25922  ig1peu  25924  coeeu  25974  plydivalg  26048  aaliou2b  26090  ulmss  26145  ulmcn  26147  efif1olem4  26290  efsubm  26296  logccv  26407  logbmpt  26529  logbfval  26531  cvxcl  26725  basellem4  26824  fsumdvdscom  26925  musum  26931  dvdsmulf1o  26934  fsumdvdsmul  26935  dchrelbasd  26978  dchrmulcl  26988  dchrinv  27000  lgsqrlem2  27086  lgsdchr  27094  lgseisenlem2  27115  lgsquadlem1  27119  lgsquadlem2  27120  2sqreulem4  27193  dchrisumlema  27227  dchrisumlem2  27229  chpdifbndlem2  27293  pntpbnd  27327  pntibndlem3  27331  ssltd  27529  oldbday  27632  addsprop  27698  mulscutlem  27826  divsmo  27873  axtgcont  27987  tgjustc1  27993  tgjustc2  27994  iscgrglt  28032  ercgrg  28035  idmot  28055  motco  28058  cnvmot  28059  motcgrg  28062  tgisline  28145  tghilberti2  28156  mirreu3  28172  mirmot  28193  ragperp  28235  foot  28240  mideu  28256  midf  28294  lmimot  28316  trgcopyeu  28324  f1otrgds  28387  f1otrg  28389  f1otrge  28390  xmstrkgc  28410  brbtwn2  28430  axlowdimlem15  28481  axcontlem2  28490  axcontlem10  28498  eengtrkg  28511  eengtrkge  28512  numedglnl  28671  usgredgreu  28742  uspgredg2vtxeu  28744  uspgredg2v  28748  usgredg2v  28751  wlkswwlksf1o  29400  wwlksnextinj  29420  clwlkclwwlkf1  29530  clwwlkf1  29569  frcond4  29790  frgrncvvdeqlem8  29826  frgrncvvdeq  29829  frgrwopreglem4  29835  numclwwlk1lem2f1  29877  nrt2irr  29993  grpoinvf  30052  nvmf  30165  vacn  30214  nmcvcn  30215  smcnlem  30217  sspg  30248  ssps  30250  sspmlem  30252  0lno  30310  blocni  30325  ipblnfi  30375  minvecolem7  30403  unopf1o  31436  cnvunop  31438  unoplin  31440  counop  31441  hmopadj2  31461  hmoplin  31462  bralnfn  31468  lnopeq0i  31527  hmops  31540  hmopm  31541  hmopco  31543  lnconi  31553  cnlnadjlem2  31588  adjmul  31612  adjadd  31613  cdjreui  31952  disjxpin  32086  off2  32133  2ndresdju  32141  fnpreimac  32163  suppovss  32173  f1od2  32213  xrofsup  32247  s3f1  32380  ccatf1  32382  swrdf1  32387  odutos  32405  dfmgc2lem  32432  dfmgc2  32433  pwrssmgc  32437  mgcf1o  32440  abliso  32464  symgcntz  32516  tocyccntz  32573  archiabllem1  32609  archiabllem2  32613  urpropd  32648  suborng  32703  xrge0slmod  32733  nsgmgc  32797  intlidl  32810  rhmpreimaidl  32811  idlinsubrg  32823  rhmimaidl  32824  prmidl2  32833  idlmulssprm  32834  isprmidlc  32840  rhmpreimaprmidl  32844  qsidomlem1  32845  qsidomlem2  32846  mxidlprm  32860  mxidlirredi  32861  ssmxidllem  32863  ply1degltdimlem  32995  ply1degltdim  32996  lindsun  32998  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  evls1maplmhm  33049  minplyirred  33059  1smat1  33082  submateq  33087  madjusmdetlem3  33107  zart0  33157  pstmxmet  33175  ofcf  33399  ldgenpisys  33462  rossros  33476  inelcarsg  33608  sibfof  33637  sitmf  33649  hgt750lemb  33966  erdszelem4  34483  erdszelem9  34488  erdsze2lem2  34493  cnpconn  34519  pconnconn  34520  txpconn  34521  ptpconn  34522  cvxpconn  34531  cvxsconn  34532  iccllysconn  34539  cvmseu  34565  cvmliftmo  34573  cvmlift2lem5  34596  cvmlift2lem9  34600  mrsubff1  34803  elmrsubrn  34809  mrsubco  34810  msubff1  34845  mvhf1  34848  segconeu  35287  fnessref  35545  neibastop1  35547  filnetlem3  35568  onsuct0  35629  unblimceq0lem  35685  unbdqndv2  35690  knoppndv  35713  irrdiff  36510  uncf  36770  fin2so  36778  lindsadd  36784  poimirlem4  36795  poimirlem13  36804  poimirlem14  36805  poimirlem26  36817  heicant  36826  mblfinlem2  36829  ftc1anc  36872  sdclem1  36914  isbnd3  36955  prdsbnd  36964  ismtycnv  36973  ismtyhmeolem  36975  ismtyres  36979  bfplem1  36993  bfplem2  36994  bfp  36995  rrnmet  37000  ismrer1  37009  iccbnd  37011  grpokerinj  37064  isdrngo2  37129  rngogrphom  37142  rngohomco  37145  rngoisocnv  37152  iscringd  37169  eqvreldisj1  37997  erprt  38046  lfl0f  38242  lkrlss  38268  lshpsmreu  38282  linepsubN  38926  pmapsub  38942  lautcnv  39264  lautco  39271  idltrn  39324  cdleme50f1  39717  cdleme50laut  39721  istendod  39936  dihf11  40441  dih1dimatlem  40503  lcfl7N  40675  lcfrlem9  40724  mapd1o  40822  hdmapf1oN  41039  hgmapf1oN  41077  fmpocos  41362  qsalrel  41368  imacrhmcl  41393  evlselv  41461  fsuppind  41464  sn-negex12  41591  nacsfix  41752  rmxypairf1o  41952  wepwsolem  42086  dnnumch3  42091  fnwe2  42097  mpaaeu  42194  idomsubgmo  42242  mon1psubm  42250  deg1mhm  42251  isotone1  43101  isotone2  43102  mnringmulrcld  43289  disjxp1  44057  disjf1  44180  wessf1ornlem  44182  projf1o  44194  sumnnodd  44644  lptioo2  44645  lptioo1  44646  cncfshift  44888  cncfperiod  44893  dvnprodlem1  44960  fourierdlem42  45163  nnfoctbdjlem  45469  isomennd  45545  smflimlem6  45790  fsetsnf1  46060  cfsetsnfsetf1  46067  otiunsndisjX  46285  imasetpreimafvbijlemf1  46370  iccpartgt  46393  icceuelpart  46402  ichnreuop  46438  sprsymrelfolem2  46459  sprsymrelf  46461  prproropf1o  46473  reupr  46488  reuopreuprim  46492  isomuspgrlem2c  46796  isomuspgr  46800  opmpoismgm  46843  mgmplusgiopALT  46870  2zlidl  46920  rnghmsscmap2  46959  rnghmsscmap  46960  rnghmsubcsetclem2  46962  rhmsscmap2  47005  rhmsscmap  47006  rhmsubcsetclem2  47008  rhmsscrnghm  47012  rhmsubcrngclem2  47014  srhmsubc  47062  fldhmsubc  47070  rhmsubc  47076  srhmsubcALTV  47080  fldhmsubcALTV  47088  rhmsubcALTV  47094  lindslinindsimp1  47225  1arymaptf1  47415  2arymaptf1  47426  toslat  47694  catprsc  47720  catprsc2  47721  isthincd  47744  isthincd2  47745  functhinclem4  47751  thincfth  47755  thincciso  47756