Theorem rexlimdvva 3221

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  rexlimdvvva  3222  disjxiun  5104  reuop  6295  f1prex  7289  f1o2ndf1  8123  poxp2  8145  xpord2pred  8147  sexp2  8148  xpord3pred  8154  sexp3  8155  frrlem9  8297  uniinqs  8801  eroveu  8816  eroprf  8819  ralxpmap  8907  unxpdomlem3  9232  finsschain  9330  dffi3  9405  sornom  10283  genpv  11012  genpdm  11015  1re  11236  cnegex  11419  zaddcl  12662  rexanre  15438  o1lo1  15628  lo1resb  15655  o1resb  15657  rlimcn3  15681  climcn2  15684  o1of2  15704  o1rlimmul  15710  lo1add  15718  lo1mul  15719  summo  15807  o1fsum  15904  ntrivcvgmul  15995  prodmolem2  16028  prodmo  16029  dvds2lem  16364  bezoutlem4  16638  dvdsmulgcd  16652  divgcdcoprm0  16761  cncongr1  16763  pcqmul  16951  pcneg  16972  pcadd  16987  4sqlem1  17046  4sqlem2  17047  4sqlem4  17050  mul4sq  17052  4sqlem12  17054  4sqlem13  17055  4sqlem18  17060  vdwmc2  17077  vdwlem7  17085  vdwlem9  17087  vdwlem10  17088  vdwlem11  17089  ramlb  17117  ramub1lem2  17125  imasaddfnlem  17620  imasmnd2  18887  xpsmnd0  18891  imasgrp2  19184  cyccom  19337  gaorber  19441  psgnunilem2  19628  psgneu  19639  lsmsubm  19786  lsmsubg  19787  lsmmod  19808  lsmdisj2  19815  pj1eu  19829  efgtlen  19859  efgredlem  19880  efgredeu  19885  efgcpbllemb  19888  frgpuptinv  19904  frgpup3lem  19910  qusabl  19998  frgpnabllem1  20006  frgpnabl  20008  dprdsubg  20159  ablfacrp  20201  pgpfac1lem3  20212  imasrng  20318  imasring  20477  xpsring1d  20480  dvdsrtr  20515  isnzr2  20684  lss1d  21153  lsmcl  21273  lsmelval2  21275  lbsextlem2  21352  qsssubdrg  21645  znfld  21779  cygznlem3  21788  psgnghm  21799  lsmcss  21911  psdmul  22400  mdetunilem7  22846  mdetunilem8  22847  cayleyhamilton0  23120  cayleyhamiltonALT  23122  restbas  23389  ordtbas2  23422  ordtbas  23423  cnhaus  23585  cldllycmp  23727  txbas  23799  ptbasin  23809  txcls  23836  xkoccn  23851  txindis  23866  txlly  23868  txnlly  23869  pthaus  23870  ptrescn  23871  txhaus  23879  tx1stc  23882  txkgen  23884  xkohaus  23885  xkoptsub  23886  xkopt  23887  xkoco1cn  23889  xkoco2cn  23890  xkoinjcn  23919  fmfnfmlem3  24188  fmfnfmlem4  24189  hausflimi  24212  hauspwpwf1  24219  txflf  24238  qustgplem  24353  blin2  24661  prdsxmslem2  24761  xrge0tsms  25067  addcnlem  25097  minveclem3b  25662  pmltpc  25684  evthicc2  25694  dyaddisj  25830  ismbfd  25873  mbfimaopnlem  25889  rolle  26224  dvcnvrelem1  26251  dvcvx  26254  itgsubst  26283  plyf  26430  plypf1  26445  plyadd  26450  plymul  26451  coeeu  26458  dgrlem  26462  coeid  26471  aalioulem6  26580  logbgcd1irr  27039  o1cxp  27219  dchrptlem2  27509  lgsdchr  27599  2sqlem5  27666  2sqlem9  27671  2sqb  27676  2sqreulem1  27690  2sqreunnlem1  27693  2sqreunnltblem  27695  pntlemp  27854  pnt3  27856  ostthlem1  27871  ostth3  27882  nosupprefixmo  27944  noinfprefixmo  27945  addsproplem2  28243  negsproplem2  28302  mulsproplem9  28397  sltmuls1  28420  sltmuls2  28421  precsexlem8  28487  precsexlem9  28488  precsexlem10  28489  precsexlem11  28490  onmulscl  28551  eucliddivs  28649  zaddscl  28667  zmulscld  28670  z12addscl  28750  z12sge0  28756  recut  28767  readdscl  28772  remulscl  28775  axcontlem4  29432  axcontlem9  29437  upgrpredgv  29604  edglnl  29608  numedglnl  29609  usgredg4  29685  nbuhgr2vtx1edgb  29820  2pthon3v  30419  umgr3v3e3cycl  30672  3cyclfrgr  30776  n4cyclfrgr  30779  frgrwopreg  30811  2clwwlk2clwwlk  30838  ubthlem3  31361  cdjreui  32921  cdj3i  32930  br8d  33089  xrofsup  33246  xrge0tsmsd  33521  qqhval2  34500  mbfmco2  34784  txpconn  35819  cvmlift2lem10  35899  cvmlift2lem12  35901  cvmlift3lem7  35912  cvmlift3lem8  35913  satfv0  35945  satfv0fun  35958  satffunlem2lem1  35991  mclsppslem  36170  br8  36343  br6  36344  br4  36345  brsegle  36696  ltnmul  36804  nadddilem1  36808  tailfb  37004  unbdqndv2  37216  qdiff  38087  mblfinlem3  38416  ismblfin  38418  itg2addnc  38431  ftc1anc  38458  isbnd2  38541  isbnd3  38542  ssbnd  38546  ispridlc  38828  lshpkrlem6  39996  athgt  40337  3dim1  40348  3dim2  40349  lvolex3N  40419  llncvrlpln2  40438  lplncvrlvol2  40496  linepsubN  40633  lncvrelatN  40662  linepsubclN  40832  sn-negex12  43300  fidomncyc  43425  fsuppind  43444  flt4lem7  43513  nna4b4nsq  43514  eldioph2  43615  eldioph2b  43616  diophin  43625  diophun  43626  fphpdo  43666  irrapxlem3  43673  irrapxlem5  43675  pell1234qrne0  43702  pell1234qrreccl  43703  pell1234qrmulcl  43704  pell14qrgt0  43708  pell14qrdich  43718  pell1qrge1  43719  pell1qrgap  43723  pellqrex  43728  rmxycomplete  43766  jm2.27  43857  stoweidlem49  46885  m1modmmod  48260  ichreuopeq  48381  prproropf1olem2  48412  prproropf1olem4  48414  paireqne  48419  reupr  48430  nprmmul2  48436  nprmdvdsfacm1  48535  requad2  48547  gbowgt5  48686  isgrtri  48867  grimgrtri  48873  usgrgrtrirex  48874  gpgvtx0  48977  gpgvtx1  48978  gpgedgvtx0  48985  gpgedgvtx1  48986  pgn4cyclex  49050  prelrrx2b  49652