Theorem rexlimdvva 3189

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 3188	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  rexlimdvvva  3190  disjxiun  5088  reuop  6240  f1prex  7218  f1o2ndf1  8052  poxp2  8073  xpord2pred  8075  sexp2  8076  xpord3pred  8082  sexp3  8083  frrlem9  8224  uniinqs  8721  eroveu  8736  eroprf  8739  ralxpmap  8820  unxpdomlem3  9142  finsschain  9243  dffi3  9315  sornom  10165  genpv  10887  genpdm  10890  1re  11109  cnegex  11291  zaddcl  12509  rexanre  15251  o1lo1  15441  lo1resb  15468  o1resb  15470  rlimcn3  15494  climcn2  15497  o1of2  15517  o1rlimmul  15523  lo1add  15531  lo1mul  15532  summo  15621  o1fsum  15717  ntrivcvgmul  15806  prodmolem2  15839  prodmo  15840  dvds2lem  16176  bezoutlem4  16450  dvdsmulgcd  16464  divgcdcoprm0  16573  cncongr1  16575  pcqmul  16762  pcneg  16783  pcadd  16798  4sqlem1  16857  4sqlem2  16858  4sqlem4  16861  mul4sq  16863  4sqlem12  16865  4sqlem13  16866  4sqlem18  16871  vdwmc2  16888  vdwlem7  16896  vdwlem9  16898  vdwlem10  16899  vdwlem11  16900  ramlb  16928  ramub1lem2  16936  imasaddfnlem  17429  imasmnd2  18679  xpsmnd0  18683  imasgrp2  18965  cyccom  19113  gaorber  19218  psgnunilem2  19405  psgneu  19416  lsmsubm  19563  lsmsubg  19564  lsmmod  19585  lsmdisj2  19592  pj1eu  19606  efgtlen  19636  efgredlem  19657  efgredeu  19662  efgcpbllemb  19665  frgpuptinv  19681  frgpup3lem  19687  qusabl  19775  frgpnabllem1  19783  frgpnabl  19785  dprdsubg  19936  ablfacrp  19978  pgpfac1lem3  19989  imasrng  20093  imasring  20246  xpsring1d  20249  dvdsrtr  20284  isnzr2  20431  lss1d  20894  lsmcl  21015  lsmelval2  21017  lbsextlem2  21094  qsssubdrg  21361  znfld  21495  cygznlem3  21504  psgnghm  21515  lsmcss  21627  psdmul  22079  mdetunilem7  22531  mdetunilem8  22532  cayleyhamilton0  22802  cayleyhamiltonALT  22804  restbas  23071  ordtbas2  23104  ordtbas  23105  cnhaus  23267  cldllycmp  23408  txbas  23480  ptbasin  23490  txcls  23517  xkoccn  23532  txindis  23547  txlly  23549  txnlly  23550  pthaus  23551  ptrescn  23552  txhaus  23560  tx1stc  23563  txkgen  23565  xkohaus  23566  xkoptsub  23567  xkopt  23568  xkoco1cn  23570  xkoco2cn  23571  xkoinjcn  23600  fmfnfmlem3  23869  fmfnfmlem4  23870  hausflimi  23893  hauspwpwf1  23900  txflf  23919  qustgplem  24034  blin2  24342  prdsxmslem2  24442  xrge0tsms  24748  addcnlem  24778  minveclem3b  25353  pmltpc  25376  evthicc2  25386  dyaddisj  25522  ismbfd  25565  mbfimaopnlem  25581  rolle  25919  dvcnvrelem1  25947  dvcvx  25950  itgsubst  25981  plyf  26128  plypf1  26142  plyadd  26147  plymul  26148  coeeu  26155  dgrlem  26159  coeid  26168  aalioulem6  26270  logbgcd1irr  26729  o1cxp  26910  dchrptlem2  27201  lgsdchr  27291  2sqlem5  27358  2sqlem9  27363  2sqb  27368  2sqreulem1  27382  2sqreunnlem1  27385  2sqreunnltblem  27387  pntlemp  27546  pnt3  27548  ostthlem1  27563  ostth3  27574  nosupprefixmo  27637  noinfprefixmo  27638  addsproplem2  27911  negsproplem2  27969  mulsproplem9  28061  ssltmul1  28084  ssltmul2  28085  precsexlem8  28150  precsexlem9  28151  precsexlem10  28152  precsexlem11  28153  onmulscl  28209  eucliddivs  28299  zaddscl  28316  zmulscld  28319  zs12addscl  28385  zs12ge0  28391  recut  28396  readdscl  28399  remulscl  28402  axcontlem4  28943  axcontlem9  28948  upgrpredgv  29115  edglnl  29119  numedglnl  29120  usgredg4  29193  nbuhgr2vtx1edgb  29328  2pthon3v  29919  umgr3v3e3cycl  30159  3cyclfrgr  30263  n4cyclfrgr  30266  frgrwopreg  30298  2clwwlk2clwwlk  30325  ubthlem3  30847  cdjreui  32407  cdj3i  32416  br8d  32586  xrofsup  32745  xrge0tsmsd  33037  qqhval2  33990  mbfmco2  34273  txpconn  35264  cvmlift2lem10  35344  cvmlift2lem12  35346  cvmlift3lem7  35357  cvmlift3lem8  35358  satfv0  35390  satfv0fun  35403  satffunlem2lem1  35436  mclsppslem  35615  br8  35788  br6  35789  br4  35790  brsegle  36141  tailfb  36410  unbdqndv2  36544  mblfinlem3  37698  ismblfin  37700  itg2addnc  37713  ftc1anc  37740  isbnd2  37822  isbnd3  37823  ssbnd  37827  ispridlc  38109  lshpkrlem6  39153  athgt  39494  3dim1  39505  3dim2  39506  lvolex3N  39576  llncvrlpln2  39595  lplncvrlvol2  39653  linepsubN  39790  lncvrelatN  39819  linepsubclN  39989  sn-negex12  42449  fidomncyc  42567  fsuppind  42622  flt4lem7  42691  nna4b4nsq  42692  eldioph2  42794  eldioph2b  42795  diophin  42804  diophun  42805  fphpdo  42849  irrapxlem3  42856  irrapxlem5  42858  pell1234qrne0  42885  pell1234qrreccl  42886  pell1234qrmulcl  42887  pell14qrgt0  42891  pell14qrdich  42901  pell1qrge1  42902  pell1qrgap  42906  pellqrex  42911  rmxycomplete  42949  jm2.27  43040  stoweidlem49  46086  m1modmmod  47388  ichreuopeq  47503  prproropf1olem2  47534  prproropf1olem4  47536  paireqne  47541  reupr  47552  requad2  47653  gbowgt5  47792  isgrtri  47973  grimgrtri  47979  usgrgrtrirex  47980  gpgvtx0  48083  gpgvtx1  48084  gpgedgvtx0  48091  gpgedgvtx1  48092  pgn4cyclex  48156  prelrrx2b  48745