Theorem rexlimdvva 3218

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexlimdvvva  3219  disjxiun  5096  reuop  6276  f1prex  7264  f1o2ndf1  8096  poxp2  8118  xpord2pred  8120  sexp2  8121  xpord3pred  8127  sexp3  8128  frrlem9  8270  uniinqs  8774  eroveu  8789  eroprf  8792  ralxpmap  8874  unxpdomlem3  9198  finsschain  9299  dffi3  9374  sornom  10231  genpv  10954  genpdm  10957  1re  11178  cnegex  11361  zaddcl  12608  rexanre  15357  o1lo1  15547  lo1resb  15574  o1resb  15576  rlimcn3  15600  climcn2  15603  o1of2  15623  o1rlimmul  15629  lo1add  15637  lo1mul  15638  summo  15727  o1fsum  15824  ntrivcvgmul  15915  prodmolem2  15948  prodmo  15949  dvds2lem  16285  bezoutlem4  16559  dvdsmulgcd  16573  divgcdcoprm0  16682  cncongr1  16684  pcqmul  16872  pcneg  16893  pcadd  16908  4sqlem1  16967  4sqlem2  16968  4sqlem4  16971  mul4sq  16973  4sqlem12  16975  4sqlem13  16976  4sqlem18  16981  vdwmc2  16998  vdwlem7  17006  vdwlem9  17008  vdwlem10  17009  vdwlem11  17010  ramlb  17038  ramub1lem2  17046  imasaddfnlem  17541  imasmnd2  18791  xpsmnd0  18795  imasgrp2  19080  cyccom  19227  gaorber  19331  psgnunilem2  19518  psgneu  19529  lsmsubm  19676  lsmsubg  19677  lsmmod  19698  lsmdisj2  19705  pj1eu  19719  efgtlen  19749  efgredlem  19770  efgredeu  19775  efgcpbllemb  19778  frgpuptinv  19794  frgpup3lem  19800  qusabl  19888  frgpnabllem1  19896  frgpnabl  19898  dprdsubg  20049  ablfacrp  20091  pgpfac1lem3  20102  imasrng  20206  imasring  20358  xpsring1d  20361  dvdsrtr  20396  isnzr2  20547  lss1d  21010  lsmcl  21130  lsmelval2  21132  lbsextlem2  21209  qsssubdrg  21458  znfld  21592  cygznlem3  21601  psgnghm  21612  lsmcss  21724  psdmul  22211  mdetunilem7  22658  mdetunilem8  22659  cayleyhamilton0  22929  cayleyhamiltonALT  22931  restbas  23198  ordtbas2  23231  ordtbas  23232  cnhaus  23394  cldllycmp  23535  txbas  23607  ptbasin  23617  txcls  23644  xkoccn  23659  txindis  23674  txlly  23676  txnlly  23677  pthaus  23678  ptrescn  23679  txhaus  23687  tx1stc  23690  txkgen  23692  xkohaus  23693  xkoptsub  23694  xkopt  23695  xkoco1cn  23697  xkoco2cn  23698  xkoinjcn  23727  fmfnfmlem3  23996  fmfnfmlem4  23997  hausflimi  24020  hauspwpwf1  24027  txflf  24046  qustgplem  24161  blin2  24469  prdsxmslem2  24569  xrge0tsms  24875  addcnlem  24905  minveclem3b  25470  pmltpc  25492  evthicc2  25502  dyaddisj  25638  ismbfd  25681  mbfimaopnlem  25697  rolle  26032  dvcnvrelem1  26059  dvcvx  26062  itgsubst  26091  plyf  26238  plypf1  26252  plyadd  26257  plymul  26258  coeeu  26265  dgrlem  26269  coeid  26278  aalioulem6  26378  logbgcd1irr  26836  o1cxp  27016  dchrptlem2  27306  lgsdchr  27396  2sqlem5  27463  2sqlem9  27468  2sqb  27473  2sqreulem1  27487  2sqreunnlem1  27490  2sqreunnltblem  27492  pntlemp  27651  pnt3  27653  ostthlem1  27668  ostth3  27679  nosupprefixmo  27741  noinfprefixmo  27742  addsproplem2  28040  negsproplem2  28099  mulsproplem9  28194  sltmuls1  28217  sltmuls2  28218  precsexlem8  28284  precsexlem9  28285  precsexlem10  28286  precsexlem11  28287  onmulscl  28348  eucliddivs  28446  zaddscl  28464  zmulscld  28467  z12addscl  28547  z12sge0  28553  recut  28564  readdscl  28569  remulscl  28572  axcontlem4  29114  axcontlem9  29119  upgrpredgv  29286  edglnl  29290  numedglnl  29291  usgredg4  29364  nbuhgr2vtx1edgb  29499  2pthon3v  30089  umgr3v3e3cycl  30332  3cyclfrgr  30436  n4cyclfrgr  30439  frgrwopreg  30471  2clwwlk2clwwlk  30498  ubthlem3  31021  cdjreui  32581  cdj3i  32590  br8d  32760  xrofsup  32919  xrge0tsmsd  33214  qqhval2  34240  mbfmco2  34523  txpconn  35546  cvmlift2lem10  35626  cvmlift2lem12  35628  cvmlift3lem7  35639  cvmlift3lem8  35640  satfv0  35672  satfv0fun  35685  satffunlem2lem1  35718  mclsppslem  35897  br8  36070  br6  36071  br4  36072  brsegle  36422  tailfb  36701  unbdqndv2  36913  qdiff  37783  mblfinlem3  38122  ismblfin  38124  itg2addnc  38137  ftc1anc  38164  isbnd2  38246  isbnd3  38247  ssbnd  38251  ispridlc  38533  lshpkrlem6  39703  athgt  40044  3dim1  40055  3dim2  40056  lvolex3N  40126  llncvrlpln2  40145  lplncvrlvol2  40203  linepsubN  40340  lncvrelatN  40369  linepsubclN  40539  sn-negex12  42990  fidomncyc  43117  fsuppind  43136  flt4lem7  43205  nna4b4nsq  43206  eldioph2  43307  eldioph2b  43308  diophin  43317  diophun  43318  fphpdo  43358  irrapxlem3  43365  irrapxlem5  43367  pell1234qrne0  43394  pell1234qrreccl  43395  pell1234qrmulcl  43396  pell14qrgt0  43400  pell14qrdich  43410  pell1qrge1  43411  pell1qrgap  43415  pellqrex  43420  rmxycomplete  43458  jm2.27  43549  stoweidlem49  46587  m1modmmod  47922  ichreuopeq  48043  prproropf1olem2  48074  prproropf1olem4  48076  paireqne  48081  reupr  48092  nprmmul2  48098  nprmdvdsfacm1  48197  requad2  48209  gbowgt5  48348  isgrtri  48529  grimgrtri  48535  usgrgrtrirex  48536  gpgvtx0  48639  gpgvtx1  48640  gpgedgvtx0  48647  gpgedgvtx1  48648  pgn4cyclex  48712  prelrrx2b  49300