Theorem rexlimdvva 3198

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

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

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 3061

This theorem is referenced by:  rexlimdvvva  3199  disjxiun  5116  reuop  6282  f1prex  7276  f1o2ndf1  8119  poxp2  8140  xpord2pred  8142  sexp2  8143  xpord3pred  8149  sexp3  8150  frrlem9  8291  uniinqs  8809  eroveu  8824  eroprf  8827  ralxpmap  8908  unxpdomlem3  9258  finsschain  9369  dffi3  9441  sornom  10289  genpv  11011  genpdm  11014  1re  11233  cnegex  11414  zaddcl  12630  rexanre  15363  o1lo1  15551  lo1resb  15578  o1resb  15580  rlimcn3  15604  climcn2  15607  o1of2  15627  o1rlimmul  15633  lo1add  15641  lo1mul  15642  summo  15731  o1fsum  15827  ntrivcvgmul  15916  prodmolem2  15949  prodmo  15950  dvds2lem  16286  bezoutlem4  16559  dvdsmulgcd  16573  divgcdcoprm0  16682  cncongr1  16684  pcqmul  16871  pcneg  16892  pcadd  16907  4sqlem1  16966  4sqlem2  16967  4sqlem4  16970  mul4sq  16972  4sqlem12  16974  4sqlem13  16975  4sqlem18  16980  vdwmc2  16997  vdwlem7  17005  vdwlem9  17007  vdwlem10  17008  vdwlem11  17009  ramlb  17037  ramub1lem2  17045  imasaddfnlem  17540  imasmnd2  18750  xpsmnd0  18754  imasgrp2  19036  cyccom  19184  gaorber  19289  psgnunilem2  19474  psgneu  19485  lsmsubm  19632  lsmsubg  19633  lsmmod  19654  lsmdisj2  19661  pj1eu  19675  efgtlen  19705  efgredlem  19726  efgredeu  19731  efgcpbllemb  19734  frgpuptinv  19750  frgpup3lem  19756  qusabl  19844  frgpnabllem1  19852  frgpnabl  19854  dprdsubg  20005  ablfacrp  20047  pgpfac1lem3  20058  imasrng  20135  imasring  20288  xpsring1d  20291  dvdsrtr  20326  isnzr2  20476  lss1d  20918  lsmcl  21039  lsmelval2  21041  lbsextlem2  21118  qsssubdrg  21392  znfld  21519  cygznlem3  21528  psgnghm  21538  lsmcss  21650  psdmul  22102  mdetunilem7  22554  mdetunilem8  22555  cayleyhamilton0  22825  cayleyhamiltonALT  22827  restbas  23094  ordtbas2  23127  ordtbas  23128  cnhaus  23290  cldllycmp  23431  txbas  23503  ptbasin  23513  txcls  23540  xkoccn  23555  txindis  23570  txlly  23572  txnlly  23573  pthaus  23574  ptrescn  23575  txhaus  23583  tx1stc  23586  txkgen  23588  xkohaus  23589  xkoptsub  23590  xkopt  23591  xkoco1cn  23593  xkoco2cn  23594  xkoinjcn  23623  fmfnfmlem3  23892  fmfnfmlem4  23893  hausflimi  23916  hauspwpwf1  23923  txflf  23942  qustgplem  24057  blin2  24366  prdsxmslem2  24466  xrge0tsms  24772  addcnlem  24802  minveclem3b  25378  pmltpc  25401  evthicc2  25411  dyaddisj  25547  ismbfd  25590  mbfimaopnlem  25606  rolle  25944  dvcnvrelem1  25972  dvcvx  25975  itgsubst  26006  plyf  26153  plypf1  26167  plyadd  26172  plymul  26173  coeeu  26180  dgrlem  26184  coeid  26193  aalioulem6  26295  logbgcd1irr  26754  o1cxp  26935  dchrptlem2  27226  lgsdchr  27316  2sqlem5  27383  2sqlem9  27388  2sqb  27393  2sqreulem1  27407  2sqreunnlem1  27410  2sqreunnltblem  27412  pntlemp  27571  pnt3  27573  ostthlem1  27588  ostth3  27599  nosupprefixmo  27662  noinfprefixmo  27663  addsproplem2  27920  negsproplem2  27978  mulsproplem9  28067  ssltmul1  28090  ssltmul2  28091  precsexlem8  28155  precsexlem9  28156  precsexlem10  28157  precsexlem11  28158  onmulscl  28204  zaddscl  28297  zmulscld  28300  recut  28345  readdscl  28348  remulscl  28351  axcontlem4  28892  axcontlem9  28897  upgrpredgv  29064  edglnl  29068  numedglnl  29069  usgredg4  29142  nbuhgr2vtx1edgb  29277  2pthon3v  29871  umgr3v3e3cycl  30111  3cyclfrgr  30215  n4cyclfrgr  30218  frgrwopreg  30250  2clwwlk2clwwlk  30277  ubthlem3  30799  cdjreui  32359  cdj3i  32368  br8d  32536  xrofsup  32690  xrge0tsmsd  33002  qqhval2  33959  mbfmco2  34243  txpconn  35200  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem7  35293  cvmlift3lem8  35294  satfv0  35326  satfv0fun  35339  satffunlem2lem1  35372  mclsppslem  35551  br8  35719  br6  35720  br4  35721  brsegle  36072  tailfb  36341  unbdqndv2  36475  mblfinlem3  37629  ismblfin  37631  itg2addnc  37644  ftc1anc  37671  isbnd2  37753  isbnd3  37754  ssbnd  37758  ispridlc  38040  lshpkrlem6  39079  athgt  39421  3dim1  39432  3dim2  39433  lvolex3N  39503  llncvrlpln2  39522  lplncvrlvol2  39580  linepsubN  39717  lncvrelatN  39746  linepsubclN  39916  sn-negex12  42406  fidomncyc  42505  fsuppind  42560  flt4lem7  42629  nna4b4nsq  42630  eldioph2  42732  eldioph2b  42733  diophin  42742  diophun  42743  fphpdo  42787  irrapxlem3  42794  irrapxlem5  42796  pell1234qrne0  42823  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell14qrgt0  42829  pell14qrdich  42839  pell1qrge1  42840  pell1qrgap  42844  pellqrex  42849  rmxycomplete  42888  jm2.27  42979  stoweidlem49  46026  ichreuopeq  47435  prproropf1olem2  47466  prproropf1olem4  47468  paireqne  47473  reupr  47484  requad2  47585  gbowgt5  47724  isgrtri  47903  grimgrtri  47909  usgrgrtrirex  47910  gpgvtx0  48005  gpgvtx1  48006  gpgedgvtx0  48013  gpgedgvtx1  48014  m1modmmod  48449  prelrrx2b  48642