Theorem rexlimdvva 3213

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

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

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 3071

This theorem is referenced by:  rexlimdvvva  3214  disjxiun  5140  reuop  6313  f1prex  7304  f1o2ndf1  8147  poxp2  8168  xpord2pred  8170  sexp2  8171  xpord3pred  8177  sexp3  8178  frrlem9  8319  uniinqs  8837  eroveu  8852  eroprf  8855  ralxpmap  8936  unxpdomlem3  9288  finsschain  9399  dffi3  9471  sornom  10317  genpv  11039  genpdm  11042  1re  11261  cnegex  11442  zaddcl  12657  rexanre  15385  o1lo1  15573  lo1resb  15600  o1resb  15602  rlimcn3  15626  climcn2  15629  o1of2  15649  o1rlimmul  15655  lo1add  15663  lo1mul  15664  summo  15753  o1fsum  15849  ntrivcvgmul  15938  prodmolem2  15971  prodmo  15972  dvds2lem  16306  bezoutlem4  16579  dvdsmulgcd  16593  divgcdcoprm0  16702  cncongr1  16704  pcqmul  16891  pcneg  16912  pcadd  16927  4sqlem1  16986  4sqlem2  16987  4sqlem4  16990  mul4sq  16992  4sqlem12  16994  4sqlem13  16995  4sqlem18  17000  vdwmc2  17017  vdwlem7  17025  vdwlem9  17027  vdwlem10  17028  vdwlem11  17029  ramlb  17057  ramub1lem2  17065  imasaddfnlem  17573  imasmnd2  18787  xpsmnd0  18791  imasgrp2  19073  cyccom  19221  gaorber  19326  psgnunilem2  19513  psgneu  19524  lsmsubm  19671  lsmsubg  19672  lsmmod  19693  lsmdisj2  19700  pj1eu  19714  efgtlen  19744  efgredlem  19765  efgredeu  19770  efgcpbllemb  19773  frgpuptinv  19789  frgpup3lem  19795  qusabl  19883  frgpnabllem1  19891  frgpnabl  19893  dprdsubg  20044  ablfacrp  20086  pgpfac1lem3  20097  imasrng  20174  imasring  20327  xpsring1d  20330  dvdsrtr  20368  isnzr2  20518  lss1d  20961  lsmcl  21082  lsmelval2  21084  lbsextlem2  21161  qsssubdrg  21444  znfld  21579  cygznlem3  21588  psgnghm  21598  lsmcss  21710  psdmul  22170  mdetunilem7  22624  mdetunilem8  22625  cayleyhamilton0  22895  cayleyhamiltonALT  22897  restbas  23166  ordtbas2  23199  ordtbas  23200  cnhaus  23362  cldllycmp  23503  txbas  23575  ptbasin  23585  txcls  23612  xkoccn  23627  txindis  23642  txlly  23644  txnlly  23645  pthaus  23646  ptrescn  23647  txhaus  23655  tx1stc  23658  txkgen  23660  xkohaus  23661  xkoptsub  23662  xkopt  23663  xkoco1cn  23665  xkoco2cn  23666  xkoinjcn  23695  fmfnfmlem3  23964  fmfnfmlem4  23965  hausflimi  23988  hauspwpwf1  23995  txflf  24014  qustgplem  24129  blin2  24439  prdsxmslem2  24542  xrge0tsms  24856  addcnlem  24886  minveclem3b  25462  pmltpc  25485  evthicc2  25495  dyaddisj  25631  ismbfd  25674  mbfimaopnlem  25690  rolle  26028  dvcnvrelem1  26056  dvcvx  26059  itgsubst  26090  plyf  26237  plypf1  26251  plyadd  26256  plymul  26257  coeeu  26264  dgrlem  26268  coeid  26277  aalioulem6  26379  logbgcd1irr  26837  o1cxp  27018  dchrptlem2  27309  lgsdchr  27399  2sqlem5  27466  2sqlem9  27471  2sqb  27476  2sqreulem1  27490  2sqreunnlem1  27493  2sqreunnltblem  27495  pntlemp  27654  pnt3  27656  ostthlem1  27671  ostth3  27682  nosupprefixmo  27745  noinfprefixmo  27746  addsproplem2  28003  negsproplem2  28061  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  precsexlem8  28238  precsexlem9  28239  precsexlem10  28240  precsexlem11  28241  onmulscl  28287  zaddscl  28380  zmulscld  28383  recut  28428  readdscl  28431  remulscl  28434  axcontlem4  28982  axcontlem9  28987  upgrpredgv  29156  edglnl  29160  numedglnl  29161  usgredg4  29234  nbuhgr2vtx1edgb  29369  2pthon3v  29963  umgr3v3e3cycl  30203  3cyclfrgr  30307  n4cyclfrgr  30310  frgrwopreg  30342  2clwwlk2clwwlk  30369  ubthlem3  30891  cdjreui  32451  cdj3i  32460  br8d  32622  xrofsup  32771  xrge0tsmsd  33065  qqhval2  33983  mbfmco2  34267  txpconn  35237  cvmlift2lem10  35317  cvmlift2lem12  35319  cvmlift3lem7  35330  cvmlift3lem8  35331  satfv0  35363  satfv0fun  35376  satffunlem2lem1  35409  mclsppslem  35588  br8  35756  br6  35757  br4  35758  brsegle  36109  tailfb  36378  unbdqndv2  36512  mblfinlem3  37666  ismblfin  37668  itg2addnc  37681  ftc1anc  37708  isbnd2  37790  isbnd3  37791  ssbnd  37795  ispridlc  38077  lshpkrlem6  39116  athgt  39458  3dim1  39469  3dim2  39470  lvolex3N  39540  llncvrlpln2  39559  lplncvrlvol2  39617  linepsubN  39754  lncvrelatN  39783  linepsubclN  39953  sn-negex12  42446  fidomncyc  42545  fsuppind  42600  flt4lem7  42669  nna4b4nsq  42670  eldioph2  42773  eldioph2b  42774  diophin  42783  diophun  42784  fphpdo  42828  irrapxlem3  42835  irrapxlem5  42837  pell1234qrne0  42864  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell14qrgt0  42870  pell14qrdich  42880  pell1qrge1  42881  pell1qrgap  42885  pellqrex  42890  rmxycomplete  42929  jm2.27  43020  stoweidlem49  46064  ichreuopeq  47460  prproropf1olem2  47491  prproropf1olem4  47493  paireqne  47498  reupr  47509  requad2  47610  gbowgt5  47749  isgrtri  47910  grimgrtri  47916  usgrgrtrirex  47917  gpgvtx0  48008  gpgvtx1  48009  gpgedgvtx0  48019  gpgedgvtx1  48020  m1modmmod  48442  prelrrx2b  48635