Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdvv Structured version   Visualization version   GIF version

Theorem rexlimdvv 3171
 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
StepHypRef Expression
1 rexlimdvv.1 . . . 4 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
21expdimp 452 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3164 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3165 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2135  ∃wrex 3047 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1850  df-ral 3051  df-rex 3052 This theorem is referenced by:  rexlimdvva  3172  f1oiso2  6761  omeu  7830  xpdom2  8216  elfiun  8497  rankxplim3  8913  brdom6disj  9542  fpwwe2lem12  9651  tskxpss  9782  genpss  10014  genpcd  10016  genpnmax  10017  distrlem1pr  10035  distrlem5pr  10037  ltexprlem6  10051  reclem4pr  10060  supadd  11179  supmullem1  11181  supmullem2  11182  qaddcl  11993  qmulcl  11995  sqrlem6  14183  caubnd  14293  summo  14643  bezoutlem3  15456  bezoutlem4  15457  dvdsgcd  15459  gcddiv  15466  pceu  15749  pcqcl  15759  lspfixed  19326  lspexch  19327  lsmcv  19339  lspsolvlem  19340  hausnei2  21355  uncmp  21404  txcnp  21621  tx1stc  21651  fbasrn  21885  rnelfmlem  21953  blssps  22426  blss  22427  tgqioo  22800  ovolunlem2  23462  ax5seg  26013  axpasch  26016  axeuclid  26038  upgredg2vtx  26231  pjhthmo  28466  shmodsi  28553  pjpjpre  28583  chscllem4  28804  sumdmdlem  29582  cdj3lem2a  29600  cdj3lem2b  29601  cdj3lem3a  29603  dya2iocnrect  30648  fprb  31972  btwndiff  32436  btwnconn1lem13  32508  btwnconn1lem14  32509  brsegle  32517  segletr  32523  segleantisym  32524  nn0prpwlem  32619  ismblfin  33759  heibor1lem  33917  crngohomfo  34114  lsmsat  34794  3dim1  35252  3dim3  35254  1cvratex  35258  atcvrlln2  35304  atcvrlln  35305  lplnnlelln  35328  llncvrlpln2  35342  lplnexllnN  35349  2llnjN  35352  lvolnlelln  35369  lvolnlelpln  35370  lplncvrlvol2  35400  2lplnj  35405  lneq2at  35563  lnatexN  35564  lncvrat  35567  lncmp  35568  paddasslem15  35619  paddasslem16  35620  pmodlem2  35632  pmapjoin  35637  llnexchb2  35654  lhp2lt  35786  cdlemf  36349  cdlemg1cex  36374  cdlemg2ce  36378  cdlemn11pre  36997  dihord2pre  37012  dihord4  37045  dihmeetlem20N  37113  mapdpglem24  37491  mapdpglem32  37492  baerlem3lem2  37497  baerlem5alem2  37498  baerlem5blem2  37499  hdmapglem7  37719  mzpcompact2lem  37812  pellex  37897  disjrnmpt2  39870  mullimc  40347  mullimcf  40354  addlimc  40379  limclner  40382  fourierdlem42  40865  fourierdlem80  40902  fourierdlem97  40919  sge0resplit  41122  volicorescl  41269  opnvonmbllem2  41349  smfaddlem1  41473  smflimlem6  41486  gbepos  42152  gbowpos  42153  gbegt5  42155  gboge9  42158
 Copyright terms: Public domain W3C validator