Theorem rexlimdvva 3219

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimdvvva  3220  disjxiun  5163  reuop  6324  f1prex  7320  f1o2ndf1  8163  poxp2  8184  xpord2pred  8186  sexp2  8187  xpord3pred  8193  sexp3  8194  frrlem9  8335  uniinqs  8855  eroveu  8870  eroprf  8873  ralxpmap  8954  unxpdomlem3  9315  finsschain  9429  dffi3  9500  sornom  10346  genpv  11068  genpdm  11071  1re  11290  cnegex  11471  zaddcl  12683  rexanre  15395  o1lo1  15583  lo1resb  15610  o1resb  15612  rlimcn3  15636  climcn2  15639  o1of2  15659  o1rlimmul  15665  lo1add  15673  lo1mul  15674  summo  15765  o1fsum  15861  ntrivcvgmul  15950  prodmolem2  15983  prodmo  15984  dvds2lem  16317  bezoutlem4  16589  dvdsmulgcd  16603  divgcdcoprm0  16712  cncongr1  16714  pcqmul  16900  pcneg  16921  pcadd  16936  4sqlem1  16995  4sqlem2  16996  4sqlem4  16999  mul4sq  17001  4sqlem12  17003  4sqlem13  17004  4sqlem18  17009  vdwmc2  17026  vdwlem7  17034  vdwlem9  17036  vdwlem10  17037  vdwlem11  17038  ramlb  17066  ramub1lem2  17074  imasaddfnlem  17588  imasmnd2  18809  xpsmnd0  18813  imasgrp2  19095  cyccom  19243  gaorber  19348  psgnunilem2  19537  psgneu  19548  lsmsubm  19695  lsmsubg  19696  lsmmod  19717  lsmdisj2  19724  pj1eu  19738  efgtlen  19768  efgredlem  19789  efgredeu  19794  efgcpbllemb  19797  frgpuptinv  19813  frgpup3lem  19819  qusabl  19907  frgpnabllem1  19915  frgpnabl  19917  dprdsubg  20068  ablfacrp  20110  pgpfac1lem3  20121  imasrng  20204  imasring  20353  xpsring1d  20356  dvdsrtr  20394  isnzr2  20544  lss1d  20984  lsmcl  21105  lsmelval2  21107  lbsextlem2  21184  qsssubdrg  21467  znfld  21602  cygznlem3  21611  psgnghm  21621  lsmcss  21733  psdmul  22193  mdetunilem7  22645  mdetunilem8  22646  cayleyhamilton0  22916  cayleyhamiltonALT  22918  restbas  23187  ordtbas2  23220  ordtbas  23221  cnhaus  23383  cldllycmp  23524  txbas  23596  ptbasin  23606  txcls  23633  xkoccn  23648  txindis  23663  txlly  23665  txnlly  23666  pthaus  23667  ptrescn  23668  txhaus  23676  tx1stc  23679  txkgen  23681  xkohaus  23682  xkoptsub  23683  xkopt  23684  xkoco1cn  23686  xkoco2cn  23687  xkoinjcn  23716  fmfnfmlem3  23985  fmfnfmlem4  23986  hausflimi  24009  hauspwpwf1  24016  txflf  24035  qustgplem  24150  blin2  24460  prdsxmslem2  24563  xrge0tsms  24875  addcnlem  24905  minveclem3b  25481  pmltpc  25504  evthicc2  25514  dyaddisj  25650  ismbfd  25693  mbfimaopnlem  25709  rolle  26048  dvcnvrelem1  26076  dvcvx  26079  itgsubst  26110  plyf  26257  plypf1  26271  plyadd  26276  plymul  26277  coeeu  26284  dgrlem  26288  coeid  26297  aalioulem6  26397  logbgcd1irr  26855  o1cxp  27036  dchrptlem2  27327  lgsdchr  27417  2sqlem5  27484  2sqlem9  27489  2sqb  27494  2sqreulem1  27508  2sqreunnlem1  27511  2sqreunnltblem  27513  pntlemp  27672  pnt3  27674  ostthlem1  27689  ostth3  27700  nosupprefixmo  27763  noinfprefixmo  27764  addsproplem2  28021  negsproplem2  28079  mulsproplem9  28168  ssltmul1  28191  ssltmul2  28192  precsexlem8  28256  precsexlem9  28257  precsexlem10  28258  precsexlem11  28259  onmulscl  28305  zaddscl  28398  zmulscld  28401  recut  28446  readdscl  28449  remulscl  28452  axcontlem4  29000  axcontlem9  29005  upgrpredgv  29174  edglnl  29178  numedglnl  29179  usgredg4  29252  nbuhgr2vtx1edgb  29387  2pthon3v  29976  umgr3v3e3cycl  30216  3cyclfrgr  30320  n4cyclfrgr  30323  frgrwopreg  30355  2clwwlk2clwwlk  30382  ubthlem3  30904  cdjreui  32464  cdj3i  32473  br8d  32632  xrofsup  32774  xrge0tsmsd  33041  qqhval2  33928  mbfmco2  34230  txpconn  35200  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem7  35293  cvmlift3lem8  35294  satfv0  35326  satfv0fun  35339  satffunlem2lem1  35372  mclsppslem  35551  br8  35718  br6  35719  br4  35720  brsegle  36072  tailfb  36343  unbdqndv2  36477  mblfinlem3  37619  ismblfin  37621  itg2addnc  37634  ftc1anc  37661  isbnd2  37743  isbnd3  37744  ssbnd  37748  ispridlc  38030  lshpkrlem6  39071  athgt  39413  3dim1  39424  3dim2  39425  lvolex3N  39495  llncvrlpln2  39514  lplncvrlvol2  39572  linepsubN  39709  lncvrelatN  39738  linepsubclN  39908  sn-negex12  42392  fidomncyc  42490  fsuppind  42545  flt4lem7  42614  nna4b4nsq  42615  eldioph2  42718  eldioph2b  42719  diophin  42728  diophun  42729  fphpdo  42773  irrapxlem3  42780  irrapxlem5  42782  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell14qrgt0  42815  pell14qrdich  42825  pell1qrge1  42826  pell1qrgap  42830  pellqrex  42835  rmxycomplete  42874  jm2.27  42965  stoweidlem49  45970  ichreuopeq  47347  prproropf1olem2  47378  prproropf1olem4  47380  paireqne  47385  reupr  47396  requad2  47497  gbowgt5  47636  isgrtri  47794  grimgrtri  47798  usgrgrtrirex  47799  m1modmmod  48255  prelrrx2b  48448