Theorem rexlimdvva 3222

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimdvvva  3223  disjxiun  5107  reuop  6296  f1prex  7284  f1o2ndf1  8118  poxp2  8140  xpord2pred  8142  sexp2  8143  xpord3pred  8149  sexp3  8150  frrlem9  8292  uniinqs  8796  eroveu  8811  eroprf  8814  ralxpmap  8895  unxpdomlem3  9219  finsschain  9317  dffi3  9392  sornom  10262  genpv  10985  genpdm  10988  1re  11209  cnegex  11392  zaddcl  12635  rexanre  15400  o1lo1  15590  lo1resb  15617  o1resb  15619  rlimcn3  15643  climcn2  15646  o1of2  15666  o1rlimmul  15672  lo1add  15680  lo1mul  15681  summo  15770  o1fsum  15867  ntrivcvgmul  15958  prodmolem2  15991  prodmo  15992  dvds2lem  16327  bezoutlem4  16601  dvdsmulgcd  16615  divgcdcoprm0  16724  cncongr1  16726  pcqmul  16914  pcneg  16935  pcadd  16950  4sqlem1  17009  4sqlem2  17010  4sqlem4  17013  mul4sq  17015  4sqlem12  17017  4sqlem13  17018  4sqlem18  17023  vdwmc2  17040  vdwlem7  17048  vdwlem9  17050  vdwlem10  17051  vdwlem11  17052  ramlb  17080  ramub1lem2  17088  imasaddfnlem  17583  imasmnd2  18833  xpsmnd0  18837  imasgrp2  19122  cyccom  19275  gaorber  19379  psgnunilem2  19566  psgneu  19577  lsmsubm  19724  lsmsubg  19725  lsmmod  19746  lsmdisj2  19753  pj1eu  19767  efgtlen  19797  efgredlem  19818  efgredeu  19823  efgcpbllemb  19826  frgpuptinv  19842  frgpup3lem  19848  qusabl  19936  frgpnabllem1  19944  frgpnabl  19946  dprdsubg  20097  ablfacrp  20139  pgpfac1lem3  20150  imasrng  20256  imasring  20413  xpsring1d  20416  dvdsrtr  20451  isnzr2  20602  lss1d  21065  lsmcl  21185  lsmelval2  21187  lbsextlem2  21264  qsssubdrg  21557  znfld  21691  cygznlem3  21700  psgnghm  21711  lsmcss  21823  psdmul  22310  mdetunilem7  22756  mdetunilem8  22757  cayleyhamilton0  23027  cayleyhamiltonALT  23029  restbas  23296  ordtbas2  23329  ordtbas  23330  cnhaus  23492  cldllycmp  23633  txbas  23705  ptbasin  23715  txcls  23742  xkoccn  23757  txindis  23772  txlly  23774  txnlly  23775  pthaus  23776  ptrescn  23777  txhaus  23785  tx1stc  23788  txkgen  23790  xkohaus  23791  xkoptsub  23792  xkopt  23793  xkoco1cn  23795  xkoco2cn  23796  xkoinjcn  23825  fmfnfmlem3  24094  fmfnfmlem4  24095  hausflimi  24118  hauspwpwf1  24125  txflf  24144  qustgplem  24259  blin2  24567  prdsxmslem2  24667  xrge0tsms  24973  addcnlem  25003  minveclem3b  25568  pmltpc  25590  evthicc2  25600  dyaddisj  25736  ismbfd  25779  mbfimaopnlem  25795  rolle  26130  dvcnvrelem1  26157  dvcvx  26160  itgsubst  26189  plyf  26336  plypf1  26350  plyadd  26355  plymul  26356  coeeu  26363  dgrlem  26367  coeid  26376  aalioulem6  26481  logbgcd1irr  26940  o1cxp  27120  dchrptlem2  27410  lgsdchr  27500  2sqlem5  27567  2sqlem9  27572  2sqb  27577  2sqreulem1  27591  2sqreunnlem1  27594  2sqreunnltblem  27596  pntlemp  27755  pnt3  27757  ostthlem1  27772  ostth3  27783  nosupprefixmo  27845  noinfprefixmo  27846  addsproplem2  28144  negsproplem2  28203  mulsproplem9  28298  sltmuls1  28321  sltmuls2  28322  precsexlem8  28388  precsexlem9  28389  precsexlem10  28390  precsexlem11  28391  onmulscl  28452  eucliddivs  28550  zaddscl  28568  zmulscld  28571  z12addscl  28651  z12sge0  28657  recut  28668  readdscl  28673  remulscl  28676  axcontlem4  29298  axcontlem9  29303  upgrpredgv  29470  edglnl  29474  numedglnl  29475  usgredg4  29548  nbuhgr2vtx1edgb  29683  2pthon3v  30273  umgr3v3e3cycl  30516  3cyclfrgr  30620  n4cyclfrgr  30623  frgrwopreg  30655  2clwwlk2clwwlk  30682  ubthlem3  31205  cdjreui  32765  cdj3i  32774  br8d  32934  xrofsup  33093  xrge0tsmsd  33374  qqhval2  34353  mbfmco2  34636  txpconn  35705  cvmlift2lem10  35785  cvmlift2lem12  35787  cvmlift3lem7  35798  cvmlift3lem8  35799  satfv0  35831  satfv0fun  35844  satffunlem2lem1  35877  mclsppslem  36056  br8  36229  br6  36230  br4  36231  brsegle  36581  ltnmul  36674  tailfb  36869  unbdqndv2  37081  qdiff  37952  mblfinlem3  38291  ismblfin  38293  itg2addnc  38306  ftc1anc  38333  isbnd2  38415  isbnd3  38416  ssbnd  38420  ispridlc  38702  lshpkrlem6  39870  athgt  40211  3dim1  40222  3dim2  40223  lvolex3N  40293  llncvrlpln2  40312  lplncvrlvol2  40370  linepsubN  40507  lncvrelatN  40536  linepsubclN  40706  sn-negex12  43159  fidomncyc  43286  fsuppind  43305  flt4lem7  43374  nna4b4nsq  43375  eldioph2  43476  eldioph2b  43477  diophin  43486  diophun  43487  fphpdo  43527  irrapxlem3  43534  irrapxlem5  43536  pell1234qrne0  43563  pell1234qrreccl  43564  pell1234qrmulcl  43565  pell14qrgt0  43569  pell14qrdich  43579  pell1qrge1  43580  pell1qrgap  43584  pellqrex  43589  rmxycomplete  43627  jm2.27  43718  stoweidlem49  46746  m1modmmod  48084  ichreuopeq  48205  prproropf1olem2  48236  prproropf1olem4  48238  paireqne  48243  reupr  48254  nprmmul2  48260  nprmdvdsfacm1  48359  requad2  48371  gbowgt5  48510  isgrtri  48691  grimgrtri  48697  usgrgrtrirex  48698  gpgvtx0  48801  gpgvtx1  48802  gpgedgvtx0  48809  gpgedgvtx1  48810  pgn4cyclex  48874  prelrrx2b  49477