Theorem rexlimdvva 3194

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdvvva  3195  disjxiun  5104  reuop  6266  f1prex  7259  f1o2ndf1  8101  poxp2  8122  xpord2pred  8124  sexp2  8125  xpord3pred  8131  sexp3  8132  frrlem9  8273  uniinqs  8770  eroveu  8785  eroprf  8788  ralxpmap  8869  unxpdomlem3  9199  finsschain  9310  dffi3  9382  sornom  10230  genpv  10952  genpdm  10955  1re  11174  cnegex  11355  zaddcl  12573  rexanre  15313  o1lo1  15503  lo1resb  15530  o1resb  15532  rlimcn3  15556  climcn2  15559  o1of2  15579  o1rlimmul  15585  lo1add  15593  lo1mul  15594  summo  15683  o1fsum  15779  ntrivcvgmul  15868  prodmolem2  15901  prodmo  15902  dvds2lem  16238  bezoutlem4  16512  dvdsmulgcd  16526  divgcdcoprm0  16635  cncongr1  16637  pcqmul  16824  pcneg  16845  pcadd  16860  4sqlem1  16919  4sqlem2  16920  4sqlem4  16923  mul4sq  16925  4sqlem12  16927  4sqlem13  16928  4sqlem18  16933  vdwmc2  16950  vdwlem7  16958  vdwlem9  16960  vdwlem10  16961  vdwlem11  16962  ramlb  16990  ramub1lem2  16998  imasaddfnlem  17491  imasmnd2  18701  xpsmnd0  18705  imasgrp2  18987  cyccom  19135  gaorber  19240  psgnunilem2  19425  psgneu  19436  lsmsubm  19583  lsmsubg  19584  lsmmod  19605  lsmdisj2  19612  pj1eu  19626  efgtlen  19656  efgredlem  19677  efgredeu  19682  efgcpbllemb  19685  frgpuptinv  19701  frgpup3lem  19707  qusabl  19795  frgpnabllem1  19803  frgpnabl  19805  dprdsubg  19956  ablfacrp  19998  pgpfac1lem3  20009  imasrng  20086  imasring  20239  xpsring1d  20242  dvdsrtr  20277  isnzr2  20427  lss1d  20869  lsmcl  20990  lsmelval2  20992  lbsextlem2  21069  qsssubdrg  21343  znfld  21470  cygznlem3  21479  psgnghm  21489  lsmcss  21601  psdmul  22053  mdetunilem7  22505  mdetunilem8  22506  cayleyhamilton0  22776  cayleyhamiltonALT  22778  restbas  23045  ordtbas2  23078  ordtbas  23079  cnhaus  23241  cldllycmp  23382  txbas  23454  ptbasin  23464  txcls  23491  xkoccn  23506  txindis  23521  txlly  23523  txnlly  23524  pthaus  23525  ptrescn  23526  txhaus  23534  tx1stc  23537  txkgen  23539  xkohaus  23540  xkoptsub  23541  xkopt  23542  xkoco1cn  23544  xkoco2cn  23545  xkoinjcn  23574  fmfnfmlem3  23843  fmfnfmlem4  23844  hausflimi  23867  hauspwpwf1  23874  txflf  23893  qustgplem  24008  blin2  24317  prdsxmslem2  24417  xrge0tsms  24723  addcnlem  24753  minveclem3b  25328  pmltpc  25351  evthicc2  25361  dyaddisj  25497  ismbfd  25540  mbfimaopnlem  25556  rolle  25894  dvcnvrelem1  25922  dvcvx  25925  itgsubst  25956  plyf  26103  plypf1  26117  plyadd  26122  plymul  26123  coeeu  26130  dgrlem  26134  coeid  26143  aalioulem6  26245  logbgcd1irr  26704  o1cxp  26885  dchrptlem2  27176  lgsdchr  27266  2sqlem5  27333  2sqlem9  27338  2sqb  27343  2sqreulem1  27357  2sqreunnlem1  27360  2sqreunnltblem  27362  pntlemp  27521  pnt3  27523  ostthlem1  27538  ostth3  27549  nosupprefixmo  27612  noinfprefixmo  27613  addsproplem2  27877  negsproplem2  27935  mulsproplem9  28027  ssltmul1  28050  ssltmul2  28051  precsexlem8  28116  precsexlem9  28117  precsexlem10  28118  precsexlem11  28119  onmulscl  28175  eucliddivs  28265  zaddscl  28282  zmulscld  28285  zs12ge0  28342  recut  28347  readdscl  28350  remulscl  28353  axcontlem4  28894  axcontlem9  28899  upgrpredgv  29066  edglnl  29070  numedglnl  29071  usgredg4  29144  nbuhgr2vtx1edgb  29279  2pthon3v  29873  umgr3v3e3cycl  30113  3cyclfrgr  30217  n4cyclfrgr  30220  frgrwopreg  30252  2clwwlk2clwwlk  30279  ubthlem3  30801  cdjreui  32361  cdj3i  32370  br8d  32538  xrofsup  32690  xrge0tsmsd  33002  qqhval2  33972  mbfmco2  34256  txpconn  35219  cvmlift2lem10  35299  cvmlift2lem12  35301  cvmlift3lem7  35312  cvmlift3lem8  35313  satfv0  35345  satfv0fun  35358  satffunlem2lem1  35391  mclsppslem  35570  br8  35743  br6  35744  br4  35745  brsegle  36096  tailfb  36365  unbdqndv2  36499  mblfinlem3  37653  ismblfin  37655  itg2addnc  37668  ftc1anc  37695  isbnd2  37777  isbnd3  37778  ssbnd  37782  ispridlc  38064  lshpkrlem6  39108  athgt  39450  3dim1  39461  3dim2  39462  lvolex3N  39532  llncvrlpln2  39551  lplncvrlvol2  39609  linepsubN  39746  lncvrelatN  39775  linepsubclN  39945  sn-negex12  42405  fidomncyc  42523  fsuppind  42578  flt4lem7  42647  nna4b4nsq  42648  eldioph2  42750  eldioph2b  42751  diophin  42760  diophun  42761  fphpdo  42805  irrapxlem3  42812  irrapxlem5  42814  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell14qrgt0  42847  pell14qrdich  42857  pell1qrge1  42858  pell1qrgap  42862  pellqrex  42867  rmxycomplete  42906  jm2.27  42997  stoweidlem49  46047  m1modmmod  47359  ichreuopeq  47474  prproropf1olem2  47505  prproropf1olem4  47507  paireqne  47512  reupr  47523  requad2  47624  gbowgt5  47763  isgrtri  47942  grimgrtri  47948  usgrgrtrirex  47949  gpgvtx0  48044  gpgvtx1  48045  gpgedgvtx0  48052  gpgedgvtx1  48053  pgn4cyclex  48116  prelrrx2b  48703