Theorem ralrimivva 3200

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  disjord  5130  disjxiun  5139  otsndisj  5513  otiunsndisj  5514  swopo  5593  issod  5615  reuop  6282  fcof1  7270  fliftfund  7295  isof1oidb  7306  isof1oopb  7307  soisores  7309  soisoi  7310  isocnv  7312  f1oiso  7333  oveqrspc2v  7421  oprres  7559  caovclg  7583  caovcomg  7586  off  7672  caofrss  7690  caonncan  7695  dmmpog  8045  fnmpoovd  8057  fmpoco  8065  fsplitfpar  8088  poxp  8098  fvmpocurryd  8240  smo11  8348  smoiso2  8353  omsmo  8642  nnasmo  8647  coflton  8655  qsdisj2  8774  eroprf  8794  dom2lem  8973  omxpenlem  9058  xpf1o  9124  unxpdomlem3  9237  fofinf1o  9312  dffi3  9410  supmo  9431  infmo  9474  inf3lem6  9612  cantnf  9672  rankxplim  9858  fseqenlem1  10003  fodomacn  10035  iunfictbso  10093  cofsmo  10248  infpssrlem5  10286  enfin2i  10300  fin23lem23  10305  fin23lem27  10307  fin23lem28  10319  compssiso  10353  ltordlem  11723  cju  12192  axdc4uzlem  13932  seqcaopr2  13988  seqhomo  13999  wrd2ind  14657  cshf1  14744  s3sndisj  14898  s3iunsndisj  14899  climcn2  15521  addcn2  15522  mulcn2  15524  o1of2  15541  isercolllem1  15595  fsum2dlem  15700  fsumcom2  15704  fprodser  15877  fprod2dlem  15908  fprodcom2  15912  isprm6  16635  crth  16695  eulerthlem2  16699  vdwlem12  16909  cshwsdisj  17016  imasaddfnlem  17458  imasvscafn  17467  mreexexd  17576  iscatd  17601  oppccomfpropd  17657  isofn  17706  sectmon  17713  ssctr  17756  ssceq  17757  catsubcat  17773  issubc3  17783  fullsubc  17784  fullresc  17785  isfuncd  17799  idfucl  17815  cofucl  17822  funcres2b  17831  fulloppc  17857  fthoppc  17858  idffth  17868  cofull  17869  cofth  17870  ressffth  17873  setcmon  18021  setcepi  18022  resssetc  18026  resscatc  18043  catciso  18045  fthestrcsetc  18086  fullestrcsetc  18087  embedsetcestrclem  18093  fthsetcestrc  18101  fullsetcestrc  18102  evlfcl  18159  uncfcurf  18176  hofcl  18196  yonedalem3  18217  yonedainv  18218  yonffthlem  18219  yoniso  18222  isdrs2  18243  isposd  18260  pospropd  18264  poslubmo  18348  posglbmo  18349  mgmplusf  18555  issstrmgm  18556  opifismgm  18562  ismndd  18626  mndpropd  18629  issubmnd  18631  mndinvmod  18634  ismhmd  18652  mhmpropd  18656  idmhm  18659  mhmf1o  18660  issubmd  18665  mndissubm  18666  0mhm  18678  resmhm  18679  resmhm2  18680  resmhm2b  18681  mhmco  18682  submacs  18685  prdspjmhm  18687  pwsdiagmhm  18689  pwsco1mhm  18690  pwsco2mhm  18691  gsumwspan  18704  frmdsssubm  18719  frmdup1  18722  grpsubf  18878  dfgrp3  18898  mhmmnd  18921  mhmfmhm  18922  issubg4  18999  grpissubg  19000  isnsg3  19014  nsgacs  19016  0nsg  19023  nsgid  19024  cycsubmcom  19049  isghmd  19069  ghmmhm  19070  idghm  19075  ghmnsgima  19084  ghmnsgpreima  19085  ghmf1  19089  ghmf1o  19090  gaid  19131  subgga  19132  gass  19133  gasubg  19134  cntzsubm  19168  cntrsubgnsg  19173  lactghmga  19239  symgfixf1  19271  odf1  19396  sylow1lem2  19433  sylow2blem2  19455  sylow3lem1  19461  lsmssv  19477  smndlsmidm  19490  pj1eu  19530  efglem  19550  efgtf  19556  efgred  19582  efgredeu  19586  frgpmhm  19599  frgpuptf  19604  frgpuplem  19606  mulgmhm  19658  ghmcmn  19662  invghm  19664  ablnsg  19677  cygabl  19720  gsum2d2lem  19802  gsum2d2  19803  gsumcom2  19804  dprd2d2  19875  ablfaclem2  19917  srgfcl  19979  srgcom4lem  19996  srglmhm  20004  srgrmhm  20005  ringcomlem  20055  isrhm2d  20217  kerf1ghm  20234  issubrg2  20334  subrgint  20337  primefld  20372  islmodd  20428  lmodscaf  20445  lmodprop2d  20485  islssd  20497  islss4  20524  lssacs  20529  lsspropd  20579  islmhmd  20601  lmhmima  20609  lmhmpreima  20610  reslmhm  20614  lspextmo  20618  lsmcl  20645  pj1lmhm  20662  islbs2  20718  issubrngd2  20761  opprdomn  20855  abvn0b  20856  expmhm  20950  nn0srg  20951  prmirredlem  20977  expghm  20980  mulgghm2  20981  domnchr  21019  znf1o  21042  zntoslem  21047  znfld  21051  cygznlem3  21060  phlipf  21140  dsmmlss  21234  uvcf1  21282  frlmlbs  21287  lindff1  21310  lindfrn  21311  f1lindf  21312  issubassa2  21379  mvrf1  21478  mplsubglem  21489  mplsubrg  21495  mplcoe5lem  21524  mplcoe2  21526  mplind  21562  evlslem2  21573  evlseu  21577  mhplss  21629  ply1sclf1  21744  mamucl  21832  mamuass  21833  mamudi  21834  mamudir  21835  mamuvs1  21836  mamuvs2  21837  matbas2d  21856  mamumat1cl  21872  mamulid  21874  mamurid  21875  mat1mhm  21917  dmatid  21928  dmatsubcl  21931  dmatsgrp  21932  dmatmulcl  21933  dmatsrng  21934  dmatcrng  21935  scmatscmiddistr  21941  scmatscm  21946  scmatsgrp  21952  scmatsrng  21953  scmatcrng  21954  scmatsgrp1  21955  scmatsrng1  21956  scmatf1  21964  scmatmhm  21967  mavmul0g  21986  mdet1  22034  mdetunilem9  22053  mdetuni0  22054  mdetmul  22056  madutpos  22075  smadiadetlem4  22102  1elcpmat  22148  cpmatacl  22149  cpmatmcl  22152  mat2pmatf1  22162  mat2pmatmul  22164  mat2pmat1  22165  mat2pmatlin  22168  m2cpm  22174  m2cpminvid  22186  m2cpminvid2  22188  decpmatmul  22205  pmatcollpw1  22209  monmatcollpw  22212  pmatcollpw  22214  pmatcollpw3lem  22216  pmatcollpwscmatlem2  22223  pm2mpf1  22232  mp2pm2mplem4  22242  pm2mpmhmlem2  22252  chp0mat  22279  chpidmat  22280  tgclb  22404  mretopd  22527  toponmre  22528  iscldtop  22530  ordtbaslem  22623  ordtbas2  22626  cnt0  22781  haust1  22787  cnhaus  22789  isreg2  22812  dishaus  22817  ordthaus  22819  dfconn2  22854  iunconn  22863  clsconn  22865  2ndcomap  22893  dis2ndc  22895  llynlly  22912  restnlly  22917  restlly  22918  islly2  22919  llyidm  22923  nllyidm  22924  hausllycmp  22929  kgentopon  22973  txbas  23002  ptbasin2  23013  ptbasfi  23016  txcnp  23055  txcnmpt  23059  pthaus  23073  tx1stc  23085  xkococnlem  23094  xkococn  23095  cnmpt21  23106  qtoptop2  23134  qtopeu  23151  kqt0lem  23171  isr0  23172  regr1lem2  23175  kqreglem1  23176  kqreglem2  23177  kqnrmlem1  23178  kqnrmlem2  23179  nrmr0reg  23184  reghmph  23228  nrmhmph  23229  txswaphmeo  23240  qtophmeo  23252  fbun  23275  trfbas2  23278  isfil2  23291  infil  23298  trfil2  23322  filssufilg  23346  hausflim  23416  fclsnei  23454  fclsfnflim  23462  flimfnfcls  23463  ptcmplem1  23487  clssubg  23544  tgpconncomp  23548  qustgplem  23556  tsmsfbas  23563  utoptop  23670  iducn  23719  cstucnd  23720  isxmetd  23763  isxmet2d  23764  xmettpos  23786  prdsdsf  23804  prdsmet  23807  ressprdsds  23808  imasdsf1olem  23810  imasf1oxmet  23812  imasf1omet  23813  blfvalps  23820  xmetresbl  23874  metss2  23952  comet  23953  stdbdmet  23956  stdbdmopn  23958  methaus  23960  met2ndci  23962  metustfbas  23997  nrmmetd  24014  subgngp  24075  ngptgp  24076  sranlm  24132  nlmvscnlem1  24134  nlmvscn  24135  nrginvrcn  24140  lssnlm  24149  nghmcn  24193  qtopbaslem  24206  reconn  24275  xmetdcn2  24284  metdscn  24303  metnrm  24309  elcncf1di  24342  cncfcdm  24345  mulc1cncf  24352  cncfco  24354  reparphti  24444  isncvsngpd  24598  tcphcph  24685  ipcnlem1  24693  ipcn  24694  iscfil3  24721  bcthlem5  24776  rrxmet  24856  minveclem3  24877  minveclem7  24883  ovolicc2lem4  24968  dyadmbl  25048  volcn  25054  itg1addlem1  25140  itg1addlem2  25145  itg1addlem4  25147  itg1addlem4OLD  25148  mbfi1fseqlem1  25164  mbfi1fseqlem3  25166  mbfi1fseqlem4  25167  mbfi1fseqlem5  25168  dvmptfsum  25423  c1liplem1  25444  dvgt0lem2  25451  ftc1a  25485  ply1domn  25572  ply1divmo  25584  fta1b  25618  ig1peu  25620  coeeu  25670  plydivalg  25743  aaliou2b  25785  ulmss  25840  ulmcn  25842  efif1olem4  25985  efsubm  25991  logccv  26102  logbmpt  26222  logbfval  26224  cvxcl  26418  basellem4  26517  fsumdvdscom  26618  musum  26624  dvdsmulf1o  26627  fsumdvdsmul  26628  dchrelbasd  26671  dchrmulcl  26681  dchrinv  26693  lgsqrlem2  26779  lgsdchr  26787  lgseisenlem2  26808  lgsquadlem1  26812  lgsquadlem2  26813  2sqreulem4  26886  dchrisumlema  26920  dchrisumlem2  26922  chpdifbndlem2  26986  pntpbnd  27020  pntibndlem3  27024  ssltd  27222  oldbday  27324  addsprop  27389  mulscutlem  27516  divsmo  27563  axtgcont  27649  tgjustc1  27655  tgjustc2  27656  iscgrglt  27694  ercgrg  27697  idmot  27717  motco  27720  cnvmot  27721  motcgrg  27724  tgisline  27807  tghilberti2  27818  mirreu3  27834  mirmot  27855  ragperp  27897  foot  27902  mideu  27918  midf  27956  lmimot  27978  trgcopyeu  27986  f1otrgds  28049  f1otrg  28051  f1otrge  28052  xmstrkgc  28072  brbtwn2  28092  axlowdimlem15  28143  axcontlem2  28152  axcontlem10  28160  eengtrkg  28173  eengtrkge  28174  numedglnl  28333  usgredgreu  28404  uspgredg2vtxeu  28406  uspgredg2v  28410  usgredg2v  28413  wlkswwlksf1o  29062  wwlksnextinj  29082  clwlkclwwlkf1  29192  clwwlkf1  29231  frcond4  29452  frgrncvvdeqlem8  29488  frgrncvvdeq  29491  frgrwopreglem4  29497  numclwwlk1lem2f1  29539  grpoinvf  29712  nvmf  29825  vacn  29874  nmcvcn  29875  smcnlem  29877  sspg  29908  ssps  29910  sspmlem  29912  0lno  29970  blocni  29985  ipblnfi  30035  minvecolem7  30063  unopf1o  31096  cnvunop  31098  unoplin  31100  counop  31101  hmopadj2  31121  hmoplin  31122  bralnfn  31128  lnopeq0i  31187  hmops  31200  hmopm  31201  hmopco  31203  lnconi  31213  cnlnadjlem2  31248  adjmul  31272  adjadd  31273  cdjreui  31612  disjxpin  31748  off2  31799  2ndresdju  31807  fnpreimac  31829  suppovss  31840  f1od2  31881  xrofsup  31915  s3f1  32048  ccatf1  32050  swrdf1  32055  odutos  32073  dfmgc2lem  32100  dfmgc2  32101  pwrssmgc  32105  mgcf1o  32108  abliso  32132  symgcntz  32181  tocyccntz  32238  archiabllem1  32274  archiabllem2  32278  urpropd  32309  suborng  32359  xrge0slmod  32389  nsgmgc  32443  intlidl  32455  rhmpreimaidl  32456  idlinsubrg  32464  rhmimaidl  32465  prmidl2  32474  idlmulssprm  32475  isprmidlc  32481  rhmpreimaprmidl  32485  qsidomlem1  32486  qsidomlem2  32487  mxidlprm  32501  ssmxidllem  32502  ply1degltdimlem  32609  ply1degltdim  32610  lindsun  32612  fedgmullem1  32616  fedgmullem2  32617  fedgmul  32618  evls1maplmhm  32661  1smat1  32679  submateq  32684  madjusmdetlem3  32704  zart0  32754  pstmxmet  32772  ofcf  32996  ldgenpisys  33059  rossros  33073  inelcarsg  33205  sibfof  33234  sitmf  33246  hgt750lemb  33563  erdszelem4  34080  erdszelem9  34085  erdsze2lem2  34090  cnpconn  34116  pconnconn  34117  txpconn  34118  ptpconn  34119  cvxpconn  34128  cvxsconn  34129  iccllysconn  34136  cvmseu  34162  cvmliftmo  34170  cvmlift2lem5  34193  cvmlift2lem9  34197  mrsubff1  34400  elmrsubrn  34406  mrsubco  34407  msubff1  34442  mvhf1  34445  segconeu  34877  fnessref  35110  neibastop1  35112  filnetlem3  35133  onsuct0  35194  unblimceq0lem  35250  unbdqndv2  35255  knoppndv  35278  irrdiff  36075  uncf  36335  fin2so  36343  lindsadd  36349  poimirlem4  36360  poimirlem13  36369  poimirlem14  36370  poimirlem26  36382  heicant  36391  mblfinlem2  36394  ftc1anc  36437  sdclem1  36480  isbnd3  36521  prdsbnd  36530  ismtycnv  36539  ismtyhmeolem  36541  ismtyres  36545  bfplem1  36559  bfplem2  36560  bfp  36561  rrnmet  36566  ismrer1  36575  iccbnd  36577  grpokerinj  36630  isdrngo2  36695  rngogrphom  36708  rngohomco  36711  rngoisocnv  36718  iscringd  36735  eqvreldisj1  37563  erprt  37612  lfl0f  37808  lkrlss  37834  lshpsmreu  37848  linepsubN  38492  pmapsub  38508  lautcnv  38830  lautco  38837  idltrn  38890  cdleme50f1  39283  cdleme50laut  39287  istendod  39502  dihf11  40007  dih1dimatlem  40069  lcfl7N  40241  lcfrlem9  40290  mapd1o  40388  hdmapf1oN  40605  hgmapf1oN  40643  qsalrel  40938  imacrhmcl  40957  fsuppind  41015  sn-negex12  41135  nacsfix  41285  rmxypairf1o  41485  wepwsolem  41619  dnnumch3  41624  fnwe2  41630  mpaaeu  41727  idomsubgmo  41775  mon1psubm  41783  deg1mhm  41784  isotone1  42634  isotone2  42635  mnringmulrcld  42822  disjxp1  43591  disjf1  43715  wessf1ornlem  43717  projf1o  43731  sumnnodd  44183  lptioo2  44184  lptioo1  44185  cncfshift  44427  cncfperiod  44432  dvnprodlem1  44499  fourierdlem42  44702  nnfoctbdjlem  45008  isomennd  45084  smflimlem6  45329  fsetsnf1  45598  cfsetsnfsetf1  45605  otiunsndisjX  45823  imasetpreimafvbijlemf1  45908  iccpartgt  45931  icceuelpart  45940  ichnreuop  45976  sprsymrelfolem2  45997  sprsymrelf  45999  prproropf1o  46011  reupr  46026  reuopreuprim  46030  isomuspgrlem2c  46334  isomuspgr  46338  ismgmd  46382  mgmhmpropd  46391  mgmhmf1o  46393  idmgmhm  46394  issubmgm2  46396  rabsubmgmd  46397  resmgmhm  46404  resmgmhm2  46405  resmgmhm2b  46406  mgmhmco  46407  submgmacs  46410  opmpoismgm  46413  mgmplusgiopALT  46440  isrnghm2d  46511  c0mgm  46519  c0mhm  46520  lidlmmgm  46535  2zlidl  46544  rnghmsscmap2  46583  rnghmsscmap  46584  rnghmsubcsetclem2  46586  rhmsscmap2  46629  rhmsscmap  46630  rhmsubcsetclem2  46632  rhmsscrnghm  46636  rhmsubcrngclem2  46638  srhmsubc  46686  fldhmsubc  46694  rhmsubc  46700  srhmsubcALTV  46704  fldhmsubcALTV  46712  rhmsubcALTV  46718  lindslinindsimp1  46850  1arymaptf1  47040  2arymaptf1  47051  toslat  47319  catprsc  47345  catprsc2  47346  isthincd  47369  isthincd2  47370  functhinclem4  47376  thincfth  47380  thincciso  47381