Theorem rexlimdvva 3197

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexlimdvvva  3198  disjxiun  5076  reuop  6251  f1prex  7235  f1o2ndf1  8068  poxp2  8090  xpord2pred  8092  sexp2  8093  xpord3pred  8099  sexp3  8100  frrlem9  8241  uniinqs  8741  eroveu  8756  eroprf  8759  ralxpmap  8841  unxpdomlem3  9165  finsschain  9266  dffi3  9341  sornom  10197  genpv  10920  genpdm  10923  1re  11142  cnegex  11325  zaddcl  12565  rexanre  15307  o1lo1  15497  lo1resb  15524  o1resb  15526  rlimcn3  15550  climcn2  15553  o1of2  15573  o1rlimmul  15579  lo1add  15587  lo1mul  15588  summo  15677  o1fsum  15774  ntrivcvgmul  15865  prodmolem2  15898  prodmo  15899  dvds2lem  16235  bezoutlem4  16509  dvdsmulgcd  16523  divgcdcoprm0  16632  cncongr1  16634  pcqmul  16822  pcneg  16843  pcadd  16858  4sqlem1  16917  4sqlem2  16918  4sqlem4  16921  mul4sq  16923  4sqlem12  16925  4sqlem13  16926  4sqlem18  16931  vdwmc2  16948  vdwlem7  16956  vdwlem9  16958  vdwlem10  16959  vdwlem11  16960  ramlb  16988  ramub1lem2  16996  imasaddfnlem  17490  imasmnd2  18740  xpsmnd0  18744  imasgrp2  19029  cyccom  19176  gaorber  19281  psgnunilem2  19468  psgneu  19479  lsmsubm  19626  lsmsubg  19627  lsmmod  19648  lsmdisj2  19655  pj1eu  19669  efgtlen  19699  efgredlem  19720  efgredeu  19725  efgcpbllemb  19728  frgpuptinv  19744  frgpup3lem  19750  qusabl  19838  frgpnabllem1  19846  frgpnabl  19848  dprdsubg  19999  ablfacrp  20041  pgpfac1lem3  20052  imasrng  20156  imasring  20308  xpsring1d  20311  dvdsrtr  20346  isnzr2  20497  lss1d  20960  lsmcl  21080  lsmelval2  21082  lbsextlem2  21159  qsssubdrg  21408  znfld  21542  cygznlem3  21551  psgnghm  21562  lsmcss  21674  psdmul  22161  mdetunilem7  22608  mdetunilem8  22609  cayleyhamilton0  22879  cayleyhamiltonALT  22881  restbas  23148  ordtbas2  23181  ordtbas  23182  cnhaus  23344  cldllycmp  23485  txbas  23557  ptbasin  23567  txcls  23594  xkoccn  23609  txindis  23624  txlly  23626  txnlly  23627  pthaus  23628  ptrescn  23629  txhaus  23637  tx1stc  23640  txkgen  23642  xkohaus  23643  xkoptsub  23644  xkopt  23645  xkoco1cn  23647  xkoco2cn  23648  xkoinjcn  23677  fmfnfmlem3  23946  fmfnfmlem4  23947  hausflimi  23970  hauspwpwf1  23977  txflf  23996  qustgplem  24111  blin2  24419  prdsxmslem2  24519  xrge0tsms  24825  addcnlem  24855  minveclem3b  25420  pmltpc  25442  evthicc2  25452  dyaddisj  25588  ismbfd  25631  mbfimaopnlem  25647  rolle  25982  dvcnvrelem1  26009  dvcvx  26012  itgsubst  26041  plyf  26188  plypf1  26202  plyadd  26207  plymul  26208  coeeu  26215  dgrlem  26219  coeid  26228  aalioulem6  26328  logbgcd1irr  26783  o1cxp  26963  dchrptlem2  27253  lgsdchr  27343  2sqlem5  27410  2sqlem9  27415  2sqb  27420  2sqreulem1  27434  2sqreunnlem1  27437  2sqreunnltblem  27439  pntlemp  27598  pnt3  27600  ostthlem1  27615  ostth3  27626  nosupprefixmo  27689  noinfprefixmo  27690  addsproplem2  27987  negsproplem2  28046  mulsproplem9  28141  sltmuls1  28164  sltmuls2  28165  precsexlem8  28231  precsexlem9  28232  precsexlem10  28233  precsexlem11  28234  onmulscl  28295  eucliddivs  28393  zaddscl  28411  zmulscld  28414  z12addscl  28494  z12sge0  28500  recut  28511  readdscl  28516  remulscl  28519  axcontlem4  29061  axcontlem9  29066  upgrpredgv  29233  edglnl  29237  numedglnl  29238  usgredg4  29311  nbuhgr2vtx1edgb  29446  2pthon3v  30036  umgr3v3e3cycl  30279  3cyclfrgr  30383  n4cyclfrgr  30386  frgrwopreg  30418  2clwwlk2clwwlk  30445  ubthlem3  30968  cdjreui  32528  cdj3i  32537  br8d  32707  xrofsup  32866  xrge0tsmsd  33161  qqhval2  34173  mbfmco2  34456  txpconn  35467  cvmlift2lem10  35547  cvmlift2lem12  35549  cvmlift3lem7  35560  cvmlift3lem8  35561  satfv0  35593  satfv0fun  35606  satffunlem2lem1  35639  mclsppslem  35818  br8  35991  br6  35992  br4  35993  brsegle  36343  tailfb  36612  unbdqndv2  36824  qdiff  37694  mblfinlem3  38033  ismblfin  38035  itg2addnc  38048  ftc1anc  38075  isbnd2  38157  isbnd3  38158  ssbnd  38162  ispridlc  38444  lshpkrlem6  39614  athgt  39955  3dim1  39966  3dim2  39967  lvolex3N  40037  llncvrlpln2  40056  lplncvrlvol2  40114  linepsubN  40251  lncvrelatN  40280  linepsubclN  40450  sn-negex12  42901  fidomncyc  43028  fsuppind  43047  flt4lem7  43116  nna4b4nsq  43117  eldioph2  43218  eldioph2b  43219  diophin  43228  diophun  43229  fphpdo  43269  irrapxlem3  43276  irrapxlem5  43278  pell1234qrne0  43305  pell1234qrreccl  43306  pell1234qrmulcl  43307  pell14qrgt0  43311  pell14qrdich  43321  pell1qrge1  43322  pell1qrgap  43326  pellqrex  43331  rmxycomplete  43369  jm2.27  43460  stoweidlem49  46499  m1modmmod  47834  ichreuopeq  47955  prproropf1olem2  47986  prproropf1olem4  47988  paireqne  47993  reupr  48004  nprmmul2  48010  nprmdvdsfacm1  48109  requad2  48121  gbowgt5  48260  isgrtri  48441  grimgrtri  48447  usgrgrtrirex  48448  gpgvtx0  48551  gpgvtx1  48552  gpgedgvtx0  48559  gpgedgvtx1  48560  pgn4cyclex  48624  prelrrx2b  49212