Theorem rexlimdvv 3221

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimdvva  3222  fprb  7194  f1oiso2  7352  omeu  8571  xpdom2  9061  rex2dom  9214  elfiun  9391  rankxplim3  9854  brdom6disj  10517  fpwwe2lem11  10627  tskxpss  10758  genpss  10990  genpcd  10992  genpnmax  10993  distrlem1pr  11011  distrlem5pr  11013  ltexprlem6  11027  reclem4pr  11036  supadd  12184  supmullem1  12186  supmullem2  12187  qaddcl  12990  qmulcl  12992  01sqrexlem6  15300  caubnd  15412  summo  15770  bezoutlem3  16600  bezoutlem4  16601  dvdsgcd  16603  gcddiv  16610  pceu  16907  pcqcl  16917  symgpssefmnd  19467  lspfixed  21233  lspexch  21234  lsmcv  21246  lspsolvlem  21247  hausnei2  23491  uncmp  23541  txcnp  23758  tx1stc  23788  fbasrn  24022  rnelfmlem  24090  blssps  24562  blss  24563  tgqioo  24938  ovolunlem2  25638  2sqnn  27584  madebdayim  28062  ax5seg  29269  axpasch  29272  axeuclid  29294  upgredg2vtx  29472  pjhthmo  31635  shmodsi  31722  pjpjpre  31752  chscllem4  31973  sumdmdlem  32751  cdj3lem2a  32769  cdj3lem2b  32770  cdj3lem3a  32772  dya2iocnrect  34652  satffunlem2lem1  35877  btwndiff  36500  btwnconn1lem13  36572  btwnconn1lem14  36573  brsegle  36581  segletr  36587  segleantisym  36588  nn0prpwlem  36814  ismblfin  38293  heibor1lem  38441  crngohomfo  38638  lsmsat  39763  3dim1  40222  3dim3  40224  1cvratex  40228  atcvrlln2  40274  atcvrlln  40275  lplnnlelln  40298  llncvrlpln2  40312  lplnexllnN  40319  2llnjN  40322  lvolnlelln  40339  lvolnlelpln  40340  lplncvrlvol2  40370  2lplnj  40375  lneq2at  40533  lnatexN  40534  lncvrat  40537  lncmp  40538  paddasslem15  40589  paddasslem16  40590  pmodlem2  40602  pmapjoin  40607  llnexchb2  40624  lhp2lt  40756  cdlemf  41318  cdlemg1cex  41343  cdlemg2ce  41347  cdlemn11pre  41965  dihord2pre  41980  dihord4  42013  dihmeetlem20N  42081  mapdpglem24  42459  mapdpglem32  42460  baerlem3lem2  42465  baerlem5alem2  42466  baerlem5blem2  42467  hdmapglem7  42684  sn-addlid  43146  rexlimdv3d  43397  mzpcompact2lem  43465  pellex  43545  onexomgt  43951  onexoegt  43954  oaun3lem1  44084  oaun3lem2  44085  disjrnmpt2  45889  mullimc  46315  mullimcf  46322  addlimc  46345  limclner  46348  fourierdlem42  46846  fourierdlem80  46883  fourierdlem97  46900  sge0resplit  47103  volicorescl  47250  opnvonmbllem2  47330  smfaddlem1  47460  smflimlem6  47473  gbepos  48506  gbowpos  48507  gbegt5  48509  gboge9  48512  isuspgrimlem  48643  usgrgrtrirex  48698  isubgr3stgrlem6  48719  gpgcubic  48827  gpg5nbgr3star  48829  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem6  48872  pgnbgreunbgr  48873  seposep  49687  iscnrm3lem6  49699