Theorem rexlimdvva 3294

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdvva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))
2	1	ex 415	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 3293	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  disjxiun  5056  reuop  6139  f1prex  7034  f1o2ndf1  7812  uniinqs  8371  eroveu  8386  eroprf  8389  ralxpmap  8454  unxpdomlem3  8718  finsschain  8825  dffi3  8889  sornom  9693  genpv  10415  genpdm  10418  1re  10635  cnegex  10815  zaddcl  12016  rexanre  14700  o1lo1  14888  lo1resb  14915  o1resb  14917  rlimcn2  14941  climcn2  14943  o1of2  14963  o1rlimmul  14969  lo1add  14977  lo1mul  14978  summo  15068  o1fsum  15162  ntrivcvgmul  15252  prodmolem2  15283  prodmo  15284  dvds2lem  15616  bezoutlem4  15884  dvdsmulgcd  15899  divgcdcoprm0  16003  cncongr1  16005  pcqmul  16184  pcneg  16204  pcadd  16219  4sqlem1  16278  4sqlem2  16279  4sqlem4  16282  mul4sq  16284  4sqlem12  16286  4sqlem13  16287  4sqlem18  16292  vdwmc2  16309  vdwlem7  16317  vdwlem9  16319  vdwlem10  16320  vdwlem11  16321  ramlb  16349  ramub1lem2  16357  imasaddfnlem  16795  imasmnd2  17942  imasgrp2  18208  cyccom  18340  gaorber  18432  psgnunilem2  18617  psgneu  18628  lsmsubm  18772  lsmsubg  18773  lsmmod  18795  lsmdisj2  18802  pj1eu  18816  efgtlen  18846  efgredlem  18867  efgredeu  18872  efgcpbllemb  18875  frgpuptinv  18891  frgpup3lem  18897  qusabl  18979  frgpnabllem1  18987  frgpnabl  18989  cygablOLD  19005  dprdsubg  19140  ablfacrp  19182  pgpfac1lem3  19193  imasring  19363  dvdsrtr  19396  lss1d  19729  lsmcl  19849  lsmelval2  19851  lbsextlem2  19925  isnzr2  20030  qsssubdrg  20598  znfld  20701  cygznlem3  20710  psgnghm  20718  lsmcss  20830  mdetunilem7  21221  mdetunilem8  21222  cayleyhamilton0  21491  cayleyhamiltonALT  21493  restbas  21760  ordtbas2  21793  ordtbas  21794  cnhaus  21956  cldllycmp  22097  txbas  22169  ptbasin  22179  txcls  22206  xkoccn  22221  txindis  22236  txlly  22238  txnlly  22239  pthaus  22240  ptrescn  22241  txhaus  22249  tx1stc  22252  txkgen  22254  xkohaus  22255  xkoptsub  22256  xkopt  22257  xkoco1cn  22259  xkoco2cn  22260  xkoinjcn  22289  fmfnfmlem3  22558  fmfnfmlem4  22559  hausflimi  22582  hauspwpwf1  22589  txflf  22608  qustgplem  22723  blin2  23033  prdsxmslem2  23133  xrge0tsms  23436  addcnlem  23466  minveclem3b  24025  pmltpc  24045  evthicc2  24055  dyaddisj  24191  ismbfd  24234  mbfimaopnlem  24250  rolle  24581  dvcnvrelem1  24608  dvcvx  24611  itgsubst  24640  plyf  24782  plypf1  24796  plyadd  24801  plymul  24802  coeeu  24809  dgrlem  24813  coeid  24822  aalioulem6  24920  logbgcd1irr  25366  o1cxp  25546  dchrptlem2  25835  lgsdchr  25925  2sqlem5  25992  2sqlem9  25997  2sqb  26002  2sqreulem1  26016  2sqreunnlem1  26019  2sqreunnltblem  26021  pntlemp  26180  pnt3  26182  ostthlem1  26197  ostth3  26208  axcontlem4  26747  axcontlem9  26752  upgrpredgv  26918  edglnl  26922  numedglnl  26923  usgredg4  26993  nbuhgr2vtx1edgb  27128  2pthon3v  27716  umgr3v3e3cycl  27957  3cyclfrgr  28061  n4cyclfrgr  28064  frgrwopreg  28096  2clwwlk2clwwlk  28123  ubthlem3  28643  cdjreui  30203  cdj3i  30212  br8d  30355  xrofsup  30486  xrge0tsmsd  30687  qqhval2  31218  mbfmco2  31518  txpconn  32474  cvmlift2lem10  32554  cvmlift2lem12  32556  cvmlift3lem7  32567  cvmlift3lem8  32568  satfv0  32600  satfv0fun  32613  satffunlem2lem1  32646  mclsppslem  32825  br8  32987  br6  32988  br4  32989  frrlem9  33126  noprefixmo  33197  brsegle  33564  tailfb  33720  unbdqndv2  33845  mblfinlem3  34925  ismblfin  34927  itg2addnc  34940  ftc1anc  34969  isbnd2  35055  isbnd3  35056  ssbnd  35060  ispridlc  35342  lshpkrlem6  36245  athgt  36586  3dim1  36597  3dim2  36598  lvolex3N  36668  llncvrlpln2  36687  lplncvrlvol2  36745  linepsubN  36882  lncvrelatN  36911  linepsubclN  37081  eldioph2  39352  eldioph2b  39353  diophin  39362  diophun  39363  fphpdo  39407  irrapxlem3  39414  irrapxlem5  39416  pell1234qrne0  39443  pell1234qrreccl  39444  pell1234qrmulcl  39445  pell14qrgt0  39449  pell14qrdich  39459  pell1qrge1  39460  pell1qrgap  39464  pellqrex  39469  rmxycomplete  39507  jm2.27  39598  stoweidlem49  42327  ichreuopeq  43628  prproropf1olem2  43659  prproropf1olem4  43661  paireqne  43666  reupr  43677  requad2  43781  gbowgt5  43920  isomuspgrlem1  43985  isomuspgrlem2b  43987  isomuspgrlem2d  43989  m1modmmod  44574  prelrrx2b  44694