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 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexlimdvvva  3195  disjxiun  5082  reuop  6257  f1prex  7239  f1o2ndf1  8072  poxp2  8093  xpord2pred  8095  sexp2  8096  xpord3pred  8102  sexp3  8103  frrlem9  8244  uniinqs  8744  eroveu  8759  eroprf  8762  ralxpmap  8844  unxpdomlem3  9168  finsschain  9269  dffi3  9344  sornom  10199  genpv  10922  genpdm  10925  1re  11144  cnegex  11327  zaddcl  12567  rexanre  15309  o1lo1  15499  lo1resb  15526  o1resb  15528  rlimcn3  15552  climcn2  15555  o1of2  15575  o1rlimmul  15581  lo1add  15589  lo1mul  15590  summo  15679  o1fsum  15776  ntrivcvgmul  15867  prodmolem2  15900  prodmo  15901  dvds2lem  16237  bezoutlem4  16511  dvdsmulgcd  16525  divgcdcoprm0  16634  cncongr1  16636  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  17492  imasmnd2  18742  xpsmnd0  18746  imasgrp2  19031  cyccom  19178  gaorber  19283  psgnunilem2  19470  psgneu  19481  lsmsubm  19628  lsmsubg  19629  lsmmod  19650  lsmdisj2  19657  pj1eu  19671  efgtlen  19701  efgredlem  19722  efgredeu  19727  efgcpbllemb  19730  frgpuptinv  19746  frgpup3lem  19752  qusabl  19840  frgpnabllem1  19848  frgpnabl  19850  dprdsubg  20001  ablfacrp  20043  pgpfac1lem3  20054  imasrng  20158  imasring  20310  xpsring1d  20313  dvdsrtr  20348  isnzr2  20495  lss1d  20958  lsmcl  21078  lsmelval2  21080  lbsextlem2  21157  qsssubdrg  21406  znfld  21540  cygznlem3  21549  psgnghm  21560  lsmcss  21672  psdmul  22132  mdetunilem7  22583  mdetunilem8  22584  cayleyhamilton0  22854  cayleyhamiltonALT  22856  restbas  23123  ordtbas2  23156  ordtbas  23157  cnhaus  23319  cldllycmp  23460  txbas  23532  ptbasin  23542  txcls  23569  xkoccn  23584  txindis  23599  txlly  23601  txnlly  23602  pthaus  23603  ptrescn  23604  txhaus  23612  tx1stc  23615  txkgen  23617  xkohaus  23618  xkoptsub  23619  xkopt  23620  xkoco1cn  23622  xkoco2cn  23623  xkoinjcn  23652  fmfnfmlem3  23921  fmfnfmlem4  23922  hausflimi  23945  hauspwpwf1  23952  txflf  23971  qustgplem  24086  blin2  24394  prdsxmslem2  24494  xrge0tsms  24800  addcnlem  24830  minveclem3b  25395  pmltpc  25417  evthicc2  25427  dyaddisj  25563  ismbfd  25606  mbfimaopnlem  25622  rolle  25957  dvcnvrelem1  25984  dvcvx  25987  itgsubst  26016  plyf  26163  plypf1  26177  plyadd  26182  plymul  26183  coeeu  26190  dgrlem  26194  coeid  26203  aalioulem6  26303  logbgcd1irr  26758  o1cxp  26938  dchrptlem2  27228  lgsdchr  27318  2sqlem5  27385  2sqlem9  27390  2sqb  27395  2sqreulem1  27409  2sqreunnlem1  27412  2sqreunnltblem  27414  pntlemp  27573  pnt3  27575  ostthlem1  27590  ostth3  27601  nosupprefixmo  27664  noinfprefixmo  27665  addsproplem2  27962  negsproplem2  28021  mulsproplem9  28116  sltmuls1  28139  sltmuls2  28140  precsexlem8  28206  precsexlem9  28207  precsexlem10  28208  precsexlem11  28209  onmulscl  28270  eucliddivs  28368  zaddscl  28386  zmulscld  28389  z12addscl  28469  z12sge0  28475  recut  28486  readdscl  28491  remulscl  28494  axcontlem4  29036  axcontlem9  29041  upgrpredgv  29208  edglnl  29212  numedglnl  29213  usgredg4  29286  nbuhgr2vtx1edgb  29421  2pthon3v  30011  umgr3v3e3cycl  30254  3cyclfrgr  30358  n4cyclfrgr  30361  frgrwopreg  30393  2clwwlk2clwwlk  30420  ubthlem3  30943  cdjreui  32503  cdj3i  32512  br8d  32681  xrofsup  32840  xrge0tsmsd  33134  qqhval2  34126  mbfmco2  34409  txpconn  35414  cvmlift2lem10  35494  cvmlift2lem12  35496  cvmlift3lem7  35507  cvmlift3lem8  35508  satfv0  35540  satfv0fun  35553  satffunlem2lem1  35586  mclsppslem  35765  br8  35938  br6  35939  br4  35940  brsegle  36290  tailfb  36559  unbdqndv2  36771  qdiff  37641  mblfinlem3  37980  ismblfin  37982  itg2addnc  37995  ftc1anc  38022  isbnd2  38104  isbnd3  38105  ssbnd  38109  ispridlc  38391  lshpkrlem6  39561  athgt  39902  3dim1  39913  3dim2  39914  lvolex3N  39984  llncvrlpln2  40003  lplncvrlvol2  40061  linepsubN  40198  lncvrelatN  40227  linepsubclN  40397  sn-negex12  42849  fidomncyc  42980  fsuppind  43023  flt4lem7  43092  nna4b4nsq  43093  eldioph2  43194  eldioph2b  43195  diophin  43204  diophun  43205  fphpdo  43245  irrapxlem3  43252  irrapxlem5  43254  pell1234qrne0  43281  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell14qrgt0  43287  pell14qrdich  43297  pell1qrge1  43298  pell1qrgap  43302  pellqrex  43307  rmxycomplete  43345  jm2.27  43436  stoweidlem49  46477  m1modmmod  47812  ichreuopeq  47933  prproropf1olem2  47964  prproropf1olem4  47966  paireqne  47971  reupr  47982  nprmmul2  47988  nprmdvdsfacm1  48087  requad2  48099  gbowgt5  48238  isgrtri  48419  grimgrtri  48425  usgrgrtrirex  48426  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  pgn4cyclex  48602  prelrrx2b  49190