Theorem rexlimdvva 3195

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

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

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 3055

This theorem is referenced by:  rexlimdvvva  3196  disjxiun  5107  reuop  6269  f1prex  7262  f1o2ndf1  8104  poxp2  8125  xpord2pred  8127  sexp2  8128  xpord3pred  8134  sexp3  8135  frrlem9  8276  uniinqs  8773  eroveu  8788  eroprf  8791  ralxpmap  8872  unxpdomlem3  9206  finsschain  9317  dffi3  9389  sornom  10237  genpv  10959  genpdm  10962  1re  11181  cnegex  11362  zaddcl  12580  rexanre  15320  o1lo1  15510  lo1resb  15537  o1resb  15539  rlimcn3  15563  climcn2  15566  o1of2  15586  o1rlimmul  15592  lo1add  15600  lo1mul  15601  summo  15690  o1fsum  15786  ntrivcvgmul  15875  prodmolem2  15908  prodmo  15909  dvds2lem  16245  bezoutlem4  16519  dvdsmulgcd  16533  divgcdcoprm0  16642  cncongr1  16644  pcqmul  16831  pcneg  16852  pcadd  16867  4sqlem1  16926  4sqlem2  16927  4sqlem4  16930  mul4sq  16932  4sqlem12  16934  4sqlem13  16935  4sqlem18  16940  vdwmc2  16957  vdwlem7  16965  vdwlem9  16967  vdwlem10  16968  vdwlem11  16969  ramlb  16997  ramub1lem2  17005  imasaddfnlem  17498  imasmnd2  18708  xpsmnd0  18712  imasgrp2  18994  cyccom  19142  gaorber  19247  psgnunilem2  19432  psgneu  19443  lsmsubm  19590  lsmsubg  19591  lsmmod  19612  lsmdisj2  19619  pj1eu  19633  efgtlen  19663  efgredlem  19684  efgredeu  19689  efgcpbllemb  19692  frgpuptinv  19708  frgpup3lem  19714  qusabl  19802  frgpnabllem1  19810  frgpnabl  19812  dprdsubg  19963  ablfacrp  20005  pgpfac1lem3  20016  imasrng  20093  imasring  20246  xpsring1d  20249  dvdsrtr  20284  isnzr2  20434  lss1d  20876  lsmcl  20997  lsmelval2  20999  lbsextlem2  21076  qsssubdrg  21350  znfld  21477  cygznlem3  21486  psgnghm  21496  lsmcss  21608  psdmul  22060  mdetunilem7  22512  mdetunilem8  22513  cayleyhamilton0  22783  cayleyhamiltonALT  22785  restbas  23052  ordtbas2  23085  ordtbas  23086  cnhaus  23248  cldllycmp  23389  txbas  23461  ptbasin  23471  txcls  23498  xkoccn  23513  txindis  23528  txlly  23530  txnlly  23531  pthaus  23532  ptrescn  23533  txhaus  23541  tx1stc  23544  txkgen  23546  xkohaus  23547  xkoptsub  23548  xkopt  23549  xkoco1cn  23551  xkoco2cn  23552  xkoinjcn  23581  fmfnfmlem3  23850  fmfnfmlem4  23851  hausflimi  23874  hauspwpwf1  23881  txflf  23900  qustgplem  24015  blin2  24324  prdsxmslem2  24424  xrge0tsms  24730  addcnlem  24760  minveclem3b  25335  pmltpc  25358  evthicc2  25368  dyaddisj  25504  ismbfd  25547  mbfimaopnlem  25563  rolle  25901  dvcnvrelem1  25929  dvcvx  25932  itgsubst  25963  plyf  26110  plypf1  26124  plyadd  26129  plymul  26130  coeeu  26137  dgrlem  26141  coeid  26150  aalioulem6  26252  logbgcd1irr  26711  o1cxp  26892  dchrptlem2  27183  lgsdchr  27273  2sqlem5  27340  2sqlem9  27345  2sqb  27350  2sqreulem1  27364  2sqreunnlem1  27367  2sqreunnltblem  27369  pntlemp  27528  pnt3  27530  ostthlem1  27545  ostth3  27556  nosupprefixmo  27619  noinfprefixmo  27620  addsproplem2  27884  negsproplem2  27942  mulsproplem9  28034  ssltmul1  28057  ssltmul2  28058  precsexlem8  28123  precsexlem9  28124  precsexlem10  28125  precsexlem11  28126  onmulscl  28182  eucliddivs  28272  zaddscl  28289  zmulscld  28292  zs12ge0  28349  recut  28354  readdscl  28357  remulscl  28360  axcontlem4  28901  axcontlem9  28906  upgrpredgv  29073  edglnl  29077  numedglnl  29078  usgredg4  29151  nbuhgr2vtx1edgb  29286  2pthon3v  29880  umgr3v3e3cycl  30120  3cyclfrgr  30224  n4cyclfrgr  30227  frgrwopreg  30259  2clwwlk2clwwlk  30286  ubthlem3  30808  cdjreui  32368  cdj3i  32377  br8d  32545  xrofsup  32697  xrge0tsmsd  33009  qqhval2  33979  mbfmco2  34263  txpconn  35226  cvmlift2lem10  35306  cvmlift2lem12  35308  cvmlift3lem7  35319  cvmlift3lem8  35320  satfv0  35352  satfv0fun  35365  satffunlem2lem1  35398  mclsppslem  35577  br8  35750  br6  35751  br4  35752  brsegle  36103  tailfb  36372  unbdqndv2  36506  mblfinlem3  37660  ismblfin  37662  itg2addnc  37675  ftc1anc  37702  isbnd2  37784  isbnd3  37785  ssbnd  37789  ispridlc  38071  lshpkrlem6  39115  athgt  39457  3dim1  39468  3dim2  39469  lvolex3N  39539  llncvrlpln2  39558  lplncvrlvol2  39616  linepsubN  39753  lncvrelatN  39782  linepsubclN  39952  sn-negex12  42412  fidomncyc  42530  fsuppind  42585  flt4lem7  42654  nna4b4nsq  42655  eldioph2  42757  eldioph2b  42758  diophin  42767  diophun  42768  fphpdo  42812  irrapxlem3  42819  irrapxlem5  42821  pell1234qrne0  42848  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell14qrgt0  42854  pell14qrdich  42864  pell1qrge1  42865  pell1qrgap  42869  pellqrex  42874  rmxycomplete  42913  jm2.27  43004  stoweidlem49  46054  m1modmmod  47363  ichreuopeq  47478  prproropf1olem2  47509  prproropf1olem4  47511  paireqne  47516  reupr  47527  requad2  47628  gbowgt5  47767  isgrtri  47946  grimgrtri  47952  usgrgrtrirex  47953  gpgvtx0  48048  gpgvtx1  48049  gpgedgvtx0  48056  gpgedgvtx1  48057  pgn4cyclex  48120  prelrrx2b  48707