Theorem rexlimdvva 3190

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 412	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
3	2	rexlimdvv 3189	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexlimdvvva  3191  disjxiun  5090  reuop  6245  f1prex  7224  f1o2ndf1  8058  poxp2  8079  xpord2pred  8081  sexp2  8082  xpord3pred  8088  sexp3  8089  frrlem9  8230  uniinqs  8727  eroveu  8742  eroprf  8745  ralxpmap  8826  unxpdomlem3  9149  finsschain  9250  dffi3  9322  sornom  10175  genpv  10897  genpdm  10900  1re  11119  cnegex  11301  zaddcl  12518  rexanre  15256  o1lo1  15446  lo1resb  15473  o1resb  15475  rlimcn3  15499  climcn2  15502  o1of2  15522  o1rlimmul  15528  lo1add  15536  lo1mul  15537  summo  15626  o1fsum  15722  ntrivcvgmul  15811  prodmolem2  15844  prodmo  15845  dvds2lem  16181  bezoutlem4  16455  dvdsmulgcd  16469  divgcdcoprm0  16578  cncongr1  16580  pcqmul  16767  pcneg  16788  pcadd  16803  4sqlem1  16862  4sqlem2  16863  4sqlem4  16866  mul4sq  16868  4sqlem12  16870  4sqlem13  16871  4sqlem18  16876  vdwmc2  16893  vdwlem7  16901  vdwlem9  16903  vdwlem10  16904  vdwlem11  16905  ramlb  16933  ramub1lem2  16941  imasaddfnlem  17434  imasmnd2  18684  xpsmnd0  18688  imasgrp2  18970  cyccom  19117  gaorber  19222  psgnunilem2  19409  psgneu  19420  lsmsubm  19567  lsmsubg  19568  lsmmod  19589  lsmdisj2  19596  pj1eu  19610  efgtlen  19640  efgredlem  19661  efgredeu  19666  efgcpbllemb  19669  frgpuptinv  19685  frgpup3lem  19691  qusabl  19779  frgpnabllem1  19787  frgpnabl  19789  dprdsubg  19940  ablfacrp  19982  pgpfac1lem3  19993  imasrng  20097  imasring  20250  xpsring1d  20253  dvdsrtr  20288  isnzr2  20435  lss1d  20898  lsmcl  21019  lsmelval2  21021  lbsextlem2  21098  qsssubdrg  21365  znfld  21499  cygznlem3  21508  psgnghm  21519  lsmcss  21631  psdmul  22082  mdetunilem7  22534  mdetunilem8  22535  cayleyhamilton0  22805  cayleyhamiltonALT  22807  restbas  23074  ordtbas2  23107  ordtbas  23108  cnhaus  23270  cldllycmp  23411  txbas  23483  ptbasin  23493  txcls  23520  xkoccn  23535  txindis  23550  txlly  23552  txnlly  23553  pthaus  23554  ptrescn  23555  txhaus  23563  tx1stc  23566  txkgen  23568  xkohaus  23569  xkoptsub  23570  xkopt  23571  xkoco1cn  23573  xkoco2cn  23574  xkoinjcn  23603  fmfnfmlem3  23872  fmfnfmlem4  23873  hausflimi  23896  hauspwpwf1  23903  txflf  23922  qustgplem  24037  blin2  24345  prdsxmslem2  24445  xrge0tsms  24751  addcnlem  24781  minveclem3b  25356  pmltpc  25379  evthicc2  25389  dyaddisj  25525  ismbfd  25568  mbfimaopnlem  25584  rolle  25922  dvcnvrelem1  25950  dvcvx  25953  itgsubst  25984  plyf  26131  plypf1  26145  plyadd  26150  plymul  26151  coeeu  26158  dgrlem  26162  coeid  26171  aalioulem6  26273  logbgcd1irr  26732  o1cxp  26913  dchrptlem2  27204  lgsdchr  27294  2sqlem5  27361  2sqlem9  27366  2sqb  27371  2sqreulem1  27385  2sqreunnlem1  27388  2sqreunnltblem  27390  pntlemp  27549  pnt3  27551  ostthlem1  27566  ostth3  27577  nosupprefixmo  27640  noinfprefixmo  27641  addsproplem2  27914  negsproplem2  27972  mulsproplem9  28064  ssltmul1  28087  ssltmul2  28088  precsexlem8  28153  precsexlem9  28154  precsexlem10  28155  precsexlem11  28156  onmulscl  28212  eucliddivs  28302  zaddscl  28319  zmulscld  28322  zs12addscl  28388  zs12ge0  28394  recut  28399  readdscl  28402  remulscl  28405  axcontlem4  28947  axcontlem9  28952  upgrpredgv  29119  edglnl  29123  numedglnl  29124  usgredg4  29197  nbuhgr2vtx1edgb  29332  2pthon3v  29923  umgr3v3e3cycl  30166  3cyclfrgr  30270  n4cyclfrgr  30273  frgrwopreg  30305  2clwwlk2clwwlk  30332  ubthlem3  30854  cdjreui  32414  cdj3i  32423  br8d  32593  xrofsup  32754  xrge0tsmsd  33049  qqhval2  34016  mbfmco2  34299  txpconn  35297  cvmlift2lem10  35377  cvmlift2lem12  35379  cvmlift3lem7  35390  cvmlift3lem8  35391  satfv0  35423  satfv0fun  35436  satffunlem2lem1  35469  mclsppslem  35648  br8  35821  br6  35822  br4  35823  brsegle  36173  tailfb  36442  unbdqndv2  36576  mblfinlem3  37719  ismblfin  37721  itg2addnc  37734  ftc1anc  37761  isbnd2  37843  isbnd3  37844  ssbnd  37848  ispridlc  38130  lshpkrlem6  39234  athgt  39575  3dim1  39586  3dim2  39587  lvolex3N  39657  llncvrlpln2  39676  lplncvrlvol2  39734  linepsubN  39871  lncvrelatN  39900  linepsubclN  40070  sn-negex12  42535  fidomncyc  42653  fsuppind  42708  flt4lem7  42777  nna4b4nsq  42778  eldioph2  42879  eldioph2b  42880  diophin  42889  diophun  42890  fphpdo  42934  irrapxlem3  42941  irrapxlem5  42943  pell1234qrne0  42970  pell1234qrreccl  42971  pell1234qrmulcl  42972  pell14qrgt0  42976  pell14qrdich  42986  pell1qrge1  42987  pell1qrgap  42991  pellqrex  42996  rmxycomplete  43034  jm2.27  43125  stoweidlem49  46171  m1modmmod  47482  ichreuopeq  47597  prproropf1olem2  47628  prproropf1olem4  47630  paireqne  47635  reupr  47646  requad2  47747  gbowgt5  47886  isgrtri  48067  grimgrtri  48073  usgrgrtrirex  48074  gpgvtx0  48177  gpgvtx1  48178  gpgedgvtx0  48185  gpgedgvtx1  48186  pgn4cyclex  48250  prelrrx2b  48839