Theorem rexlimdvv 3219

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 458	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒)))
3	2	rexlimdv 3162	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
4	3	rexlimdva 3164	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  rexlimdvva  3220  fprb  7191  f1oiso2  7352  omeu  8577  xpdom2  9075  rex2dom  9228  elfiun  9406  rankxplim3  9879  brdom6disj  10592  fpwwe2lem11  10707  tskxpss  10838  genpss  11070  genpcd  11072  genpnmax  11073  distrlem1pr  11091  distrlem5pr  11093  ltexprlem6  11107  reclem4pr  11116  supadd  12266  supmullem1  12268  supmullem2  12269  qaddcl  13074  qmulcl  13076  01sqrexlem6  15394  caubnd  15506  summo  15863  bezoutlem3  16694  bezoutlem4  16695  dvdsgcd  16697  gcddiv  16704  pceu  17004  pcqcl  17014  symgpssefmnd  19590  crngrhmfo  20706  lspfixed  21386  lspexch  21387  lsmcv  21399  lspsolvlem  21400  hausnei2  23651  uncmp  23701  txcnp  23919  tx1stc  23949  fbasrn  24183  rnelfmlem  24251  blssps  24723  blss  24724  tgqioo  25099  ovolunlem2  25799  2sqnn  27748  madebdayim  28256  ax5seg  29498  axpasch  29501  axeuclid  29523  upgredg2vtx  29701  pjhthmo  31886  shmodsi  31973  pjpjpre  32003  chscllem4  32224  sumdmdlem  33002  cdj3lem2a  33020  cdj3lem2b  33021  cdj3lem3a  33023  dya2iocnrect  34896  satffunlem2lem1  36138  btwndiff  36762  btwnconn1lem13  36834  btwnconn1lem14  36835  brsegle  36843  segletr  36849  segleantisym  36850  nn0prpwlem  37080  ismblfin  38547  heibor1lem  38711  crngohomfo  38908  lsmsat  40033  3dim1  40492  3dim3  40494  1cvratex  40498  atcvrlln2  40544  atcvrlln  40545  lplnnlelln  40568  llncvrlpln2  40582  lplnexllnN  40589  2llnjN  40592  lvolnlelln  40609  lvolnlelpln  40610  lplncvrlvol2  40640  2lplnj  40645  lneq2at  40803  lnatexN  40804  lncvrat  40807  lncmp  40808  paddasslem15  40859  paddasslem16  40860  pmodlem2  40872  pmapjoin  40877  llnexchb2  40894  lhp2lt  41026  cdlemf  41588  cdlemg1cex  41613  cdlemg2ce  41617  cdlemn11pre  42235  dihord2pre  42250  dihord4  42283  dihmeetlem20N  42351  mapdpglem24  42729  mapdpglem32  42730  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  hdmapglem7  42954  sn-addlid  43423  rexlimdv3d  43647  mzpcompact2lem  43715  pellex  43795  onexomgt  44201  onexoegt  44204  oaun3lem1  44334  oaun3lem2  44335  disjrnmpt2  46146  mullimc  46572  mullimcf  46579  addlimc  46602  limclner  46605  fourierdlem42  47103  fourierdlem80  47140  fourierdlem97  47157  sge0resplit  47360  volicorescl  47507  opnvonmbllem2  47587  smfaddlem1  47717  smflimlem6  47730  gbepos  48800  gbowpos  48801  gbegt5  48803  gboge9  48806  isuspgrimlem  48937  usgrgrtrirex  48992  isubgr3stgrlem6  49013  gpgcubic  49121  gpg5nbgr3star  49123  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem6  49166  pgnbgreunbgr  49167  seposep  49978  iscnrm3lem6  49990