Theorem rexlimdvva 3193

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

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

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 3061

This theorem is referenced by:  rexlimdvvva  3194  disjxiun  5095  reuop  6251  f1prex  7230  f1o2ndf1  8064  poxp2  8085  xpord2pred  8087  sexp2  8088  xpord3pred  8094  sexp3  8095  frrlem9  8236  uniinqs  8734  eroveu  8749  eroprf  8752  ralxpmap  8834  unxpdomlem3  9158  finsschain  9259  dffi3  9334  sornom  10187  genpv  10910  genpdm  10913  1re  11132  cnegex  11314  zaddcl  12531  rexanre  15270  o1lo1  15460  lo1resb  15487  o1resb  15489  rlimcn3  15513  climcn2  15516  o1of2  15536  o1rlimmul  15542  lo1add  15550  lo1mul  15551  summo  15640  o1fsum  15736  ntrivcvgmul  15825  prodmolem2  15858  prodmo  15859  dvds2lem  16195  bezoutlem4  16469  dvdsmulgcd  16483  divgcdcoprm0  16592  cncongr1  16594  pcqmul  16781  pcneg  16802  pcadd  16817  4sqlem1  16876  4sqlem2  16877  4sqlem4  16880  mul4sq  16882  4sqlem12  16884  4sqlem13  16885  4sqlem18  16890  vdwmc2  16907  vdwlem7  16915  vdwlem9  16917  vdwlem10  16918  vdwlem11  16919  ramlb  16947  ramub1lem2  16955  imasaddfnlem  17449  imasmnd2  18699  xpsmnd0  18703  imasgrp2  18985  cyccom  19132  gaorber  19237  psgnunilem2  19424  psgneu  19435  lsmsubm  19582  lsmsubg  19583  lsmmod  19604  lsmdisj2  19611  pj1eu  19625  efgtlen  19655  efgredlem  19676  efgredeu  19681  efgcpbllemb  19684  frgpuptinv  19700  frgpup3lem  19706  qusabl  19794  frgpnabllem1  19802  frgpnabl  19804  dprdsubg  19955  ablfacrp  19997  pgpfac1lem3  20008  imasrng  20112  imasring  20266  xpsring1d  20269  dvdsrtr  20304  isnzr2  20451  lss1d  20914  lsmcl  21035  lsmelval2  21037  lbsextlem2  21114  qsssubdrg  21381  znfld  21515  cygznlem3  21524  psgnghm  21535  lsmcss  21647  psdmul  22109  mdetunilem7  22562  mdetunilem8  22563  cayleyhamilton0  22833  cayleyhamiltonALT  22835  restbas  23102  ordtbas2  23135  ordtbas  23136  cnhaus  23298  cldllycmp  23439  txbas  23511  ptbasin  23521  txcls  23548  xkoccn  23563  txindis  23578  txlly  23580  txnlly  23581  pthaus  23582  ptrescn  23583  txhaus  23591  tx1stc  23594  txkgen  23596  xkohaus  23597  xkoptsub  23598  xkopt  23599  xkoco1cn  23601  xkoco2cn  23602  xkoinjcn  23631  fmfnfmlem3  23900  fmfnfmlem4  23901  hausflimi  23924  hauspwpwf1  23931  txflf  23950  qustgplem  24065  blin2  24373  prdsxmslem2  24473  xrge0tsms  24779  addcnlem  24809  minveclem3b  25384  pmltpc  25407  evthicc2  25417  dyaddisj  25553  ismbfd  25596  mbfimaopnlem  25612  rolle  25950  dvcnvrelem1  25978  dvcvx  25981  itgsubst  26012  plyf  26159  plypf1  26173  plyadd  26178  plymul  26179  coeeu  26186  dgrlem  26190  coeid  26199  aalioulem6  26301  logbgcd1irr  26760  o1cxp  26941  dchrptlem2  27232  lgsdchr  27322  2sqlem5  27389  2sqlem9  27394  2sqb  27399  2sqreulem1  27413  2sqreunnlem1  27416  2sqreunnltblem  27418  pntlemp  27577  pnt3  27579  ostthlem1  27594  ostth3  27605  nosupprefixmo  27668  noinfprefixmo  27669  addsproplem2  27966  negsproplem2  28025  mulsproplem9  28120  sltmuls1  28143  sltmuls2  28144  precsexlem8  28210  precsexlem9  28211  precsexlem10  28212  precsexlem11  28213  onmulscl  28274  eucliddivs  28372  zaddscl  28390  zmulscld  28393  z12addscl  28473  z12sge0  28479  recut  28490  readdscl  28495  remulscl  28498  axcontlem4  29040  axcontlem9  29045  upgrpredgv  29212  edglnl  29216  numedglnl  29217  usgredg4  29290  nbuhgr2vtx1edgb  29425  2pthon3v  30016  umgr3v3e3cycl  30259  3cyclfrgr  30363  n4cyclfrgr  30366  frgrwopreg  30398  2clwwlk2clwwlk  30425  ubthlem3  30947  cdjreui  32507  cdj3i  32516  br8d  32686  xrofsup  32847  xrge0tsmsd  33155  qqhval2  34139  mbfmco2  34422  txpconn  35426  cvmlift2lem10  35506  cvmlift2lem12  35508  cvmlift3lem7  35519  cvmlift3lem8  35520  satfv0  35552  satfv0fun  35565  satffunlem2lem1  35598  mclsppslem  35777  br8  35950  br6  35951  br4  35952  brsegle  36302  tailfb  36571  unbdqndv2  36711  mblfinlem3  37856  ismblfin  37858  itg2addnc  37871  ftc1anc  37898  isbnd2  37980  isbnd3  37981  ssbnd  37985  ispridlc  38267  lshpkrlem6  39371  athgt  39712  3dim1  39723  3dim2  39724  lvolex3N  39794  llncvrlpln2  39813  lplncvrlvol2  39871  linepsubN  40008  lncvrelatN  40037  linepsubclN  40207  sn-negex12  42668  fidomncyc  42786  fsuppind  42829  flt4lem7  42898  nna4b4nsq  42899  eldioph2  43000  eldioph2b  43001  diophin  43010  diophun  43011  fphpdo  43055  irrapxlem3  43062  irrapxlem5  43064  pell1234qrne0  43091  pell1234qrreccl  43092  pell1234qrmulcl  43093  pell14qrgt0  43097  pell14qrdich  43107  pell1qrge1  43108  pell1qrgap  43112  pellqrex  43117  rmxycomplete  43155  jm2.27  43246  stoweidlem49  46289  m1modmmod  47600  ichreuopeq  47715  prproropf1olem2  47746  prproropf1olem4  47748  paireqne  47753  reupr  47764  requad2  47865  gbowgt5  48004  isgrtri  48185  grimgrtri  48191  usgrgrtrirex  48192  gpgvtx0  48295  gpgvtx1  48296  gpgedgvtx0  48303  gpgedgvtx1  48304  pgn4cyclex  48368  prelrrx2b  48956