Theorem rexlimdvv 3222

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

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

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 1945

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

This theorem is used by:  rexlimdvva  3223  fprb  7225  f1oiso2  7386  omeu  8624  xpdom2  9122  rex2dom  9275  elfiun  9452  rankxplim3  9928  brdom6disj  10641  fpwwe2lem11  10756  tskxpss  10887  genpss  11119  genpcd  11121  genpnmax  11122  distrlem1pr  11140  distrlem5pr  11142  ltexprlem6  11156  reclem4pr  11165  supadd  12315  supmullem1  12317  supmullem2  12318  qaddcl  13123  qmulcl  13125  01sqrexlem6  15446  caubnd  15558  summo  15915  bezoutlem3  16746  bezoutlem4  16747  dvdsgcd  16749  gcddiv  16756  pceu  17056  pcqcl  17066  symgpssefmnd  19643  crngrhmfo  20759  lspfixed  21439  lspexch  21440  lsmcv  21452  lspsolvlem  21453  hausnei2  23704  uncmp  23754  txcnp  23972  tx1stc  24002  fbasrn  24236  rnelfmlem  24304  blssps  24776  blss  24777  tgqioo  25152  ovolunlem2  25852  2sqnn  27799  madebdayim  28307  ax5seg  29549  axpasch  29552  axeuclid  29574  upgredg2vtx  29752  pjhthmo  31937  shmodsi  32024  pjpjpre  32054  chscllem4  32275  sumdmdlem  33053  cdj3lem2a  33071  cdj3lem2b  33072  cdj3lem3a  33074  dya2iocnrect  34996  satffunlem2lem1  36349  btwndiff  36983  btwnconn1lem13  37055  btwnconn1lem14  37056  brsegle  37064  segletr  37070  segleantisym  37071  nn0prpwlem  37301  ismblfin  38784  heibor1lem  38946  crngohomfo  39143  lsmsat  40268  3dim1  40727  3dim3  40729  1cvratex  40733  atcvrlln2  40779  atcvrlln  40780  lplnnlelln  40803  llncvrlpln2  40817  lplnexllnN  40824  2llnjN  40827  lvolnlelln  40844  lvolnlelpln  40845  lplncvrlvol2  40875  2lplnj  40880  lneq2at  41038  lnatexN  41039  lncvrat  41042  lncmp  41043  paddasslem15  41094  paddasslem16  41095  pmodlem2  41107  pmapjoin  41112  llnexchb2  41129  lhp2lt  41261  cdlemf  41823  cdlemg1cex  41848  cdlemg2ce  41852  cdlemn11pre  42470  dihord2pre  42485  dihord4  42518  dihmeetlem20N  42586  mapdpglem24  42964  mapdpglem32  42965  baerlem3lem2  42970  baerlem5alem2  42971  baerlem5blem2  42972  hdmapglem7  43189  sn-addlid  43659  rexlimdv3d  43897  mzpcompact2lem  43966  pellex  44046  onexomgt  44446  onexoegt  44449  oaun3lem1  44579  oaun3lem2  44580  disjrnmpt2  46418  mullimc  46843  mullimcf  46850  addlimc  46873  limclner  46876  fourierdlem42  47374  fourierdlem80  47411  fourierdlem97  47428  sge0resplit  47631  volicorescl  47778  opnvonmbllem2  47858  smfaddlem1  47988  smflimlem6  48001  gbepos  49071  gbowpos  49072  gbegt5  49074  gboge9  49077  isuspgrimlem  49208  usgrgrtrirex  49263  isubgr3stgrlem6  49284  gpgcubic  49392  gpg5nbgr3star  49394  pgnbgreunbgrlem3  49431  pgnbgreunbgrlem6  49437  pgnbgreunbgr  49438  seposep  50255  iscnrm3lem6  50267