Theorem rexlimdvv 3197

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
rexlimdvv.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimdvv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvv

Step	Hyp	Ref	Expression
1		rexlimdvv.1	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))
2	1	expdimp 452	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3139	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3141	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:  rexlimdvva  3198  fprb  7185  f1oiso2  7344  omeu  8595  xpdom2  9079  rex2dom  9252  elfiun  9440  rankxplim3  9893  brdom6disj  10544  fpwwe2lem11  10653  tskxpss  10784  genpss  11016  genpcd  11018  genpnmax  11019  distrlem1pr  11037  distrlem5pr  11039  ltexprlem6  11053  reclem4pr  11062  supadd  12208  supmullem1  12210  supmullem2  12211  qaddcl  12979  qmulcl  12981  01sqrexlem6  15264  caubnd  15375  summo  15731  bezoutlem3  16558  bezoutlem4  16559  dvdsgcd  16561  gcddiv  16568  pceu  16864  pcqcl  16874  symgpssefmnd  19375  lspfixed  21087  lspexch  21088  lsmcv  21100  lspsolvlem  21101  hausnei2  23289  uncmp  23339  txcnp  23556  tx1stc  23586  fbasrn  23820  rnelfmlem  23888  blssps  24361  blss  24362  tgqioo  24737  ovolunlem2  25449  2sqnn  27400  madebdayim  27843  ax5seg  28863  axpasch  28866  axeuclid  28888  upgredg2vtx  29066  pjhthmo  31229  shmodsi  31316  pjpjpre  31346  chscllem4  31567  sumdmdlem  32345  cdj3lem2a  32363  cdj3lem2b  32364  cdj3lem3a  32366  dya2iocnrect  34259  satffunlem2lem1  35372  btwndiff  35991  btwnconn1lem13  36063  btwnconn1lem14  36064  brsegle  36072  segletr  36078  segleantisym  36079  nn0prpwlem  36286  ismblfin  37631  heibor1lem  37779  crngohomfo  37976  lsmsat  38972  3dim1  39432  3dim3  39434  1cvratex  39438  atcvrlln2  39484  atcvrlln  39485  lplnnlelln  39508  llncvrlpln2  39522  lplnexllnN  39529  2llnjN  39532  lvolnlelln  39549  lvolnlelpln  39550  lplncvrlvol2  39580  2lplnj  39585  lneq2at  39743  lnatexN  39744  lncvrat  39747  lncmp  39748  paddasslem15  39799  paddasslem16  39800  pmodlem2  39812  pmapjoin  39817  llnexchb2  39834  lhp2lt  39966  cdlemf  40528  cdlemg1cex  40553  cdlemg2ce  40557  cdlemn11pre  41175  dihord2pre  41190  dihord4  41223  dihmeetlem20N  41291  mapdpglem24  41669  mapdpglem32  41670  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  hdmapglem7  41894  sn-addlid  42394  rexlimdv3d  42653  mzpcompact2lem  42721  pellex  42805  onexomgt  43212  onexoegt  43215  oaun3lem1  43345  oaun3lem2  43346  disjrnmpt2  45160  mullimc  45593  mullimcf  45600  addlimc  45625  limclner  45628  fourierdlem42  46126  fourierdlem80  46163  fourierdlem97  46180  sge0resplit  46383  volicorescl  46530  opnvonmbllem2  46610  smfaddlem1  46740  smflimlem6  46753  gbepos  47720  gbowpos  47721  gbegt5  47723  gboge9  47726  isuspgrimlem  47856  usgrgrtrirex  47910  isubgr3stgrlem6  47931  gpgcubic  48029  gpg5nbgr3star  48031  seposep  48848  iscnrm3lem6  48860