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

Theorem rexlimdvv 3255
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 456 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3245 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3246 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  wrex 3110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115
This theorem is referenced by:  rexlimdvva  3256  fprb  6937  f1oiso2  7088  omeu  8198  xpdom2  8599  elfiun  8882  rankxplim3  9298  brdom6disj  9947  fpwwe2lem12  10056  tskxpss  10187  genpss  10419  genpcd  10421  genpnmax  10422  distrlem1pr  10440  distrlem5pr  10442  ltexprlem6  10456  reclem4pr  10465  supadd  11600  supmullem1  11602  supmullem2  11603  qaddcl  12356  qmulcl  12358  sqrlem6  14603  caubnd  14714  summo  15070  bezoutlem3  15883  bezoutlem4  15884  dvdsgcd  15886  gcddiv  15893  pceu  16177  pcqcl  16187  symgpssefmnd  18520  lspfixed  19897  lspexch  19898  lsmcv  19910  lspsolvlem  19911  hausnei2  21962  uncmp  22012  txcnp  22229  tx1stc  22259  fbasrn  22493  rnelfmlem  22561  blssps  23035  blss  23036  tgqioo  23409  ovolunlem2  24106  2sqnn  26027  ax5seg  26736  axpasch  26739  axeuclid  26761  upgredg2vtx  26938  pjhthmo  29089  shmodsi  29176  pjpjpre  29206  chscllem4  29427  sumdmdlem  30205  cdj3lem2a  30223  cdj3lem2b  30224  cdj3lem3a  30226  dya2iocnrect  31653  satffunlem2lem1  32765  btwndiff  33602  btwnconn1lem13  33674  btwnconn1lem14  33675  brsegle  33683  segletr  33689  segleantisym  33690  nn0prpwlem  33784  ismblfin  35097  heibor1lem  35246  crngohomfo  35443  lsmsat  36303  3dim1  36762  3dim3  36764  1cvratex  36768  atcvrlln2  36814  atcvrlln  36815  lplnnlelln  36838  llncvrlpln2  36852  lplnexllnN  36859  2llnjN  36862  lvolnlelln  36879  lvolnlelpln  36880  lplncvrlvol2  36910  2lplnj  36915  lneq2at  37073  lnatexN  37074  lncvrat  37077  lncmp  37078  paddasslem15  37129  paddasslem16  37130  pmodlem2  37142  pmapjoin  37147  llnexchb2  37164  lhp2lt  37296  cdlemf  37858  cdlemg1cex  37883  cdlemg2ce  37887  cdlemn11pre  38505  dihord2pre  38520  dihord4  38553  dihmeetlem20N  38621  mapdpglem24  38999  mapdpglem32  39000  baerlem3lem2  39005  baerlem5alem2  39006  baerlem5blem2  39007  hdmapglem7  39224  sn-addid2  39535  rexlimdv3d  39617  mzpcompact2lem  39685  pellex  39769  disjrnmpt2  41808  mullimc  42251  mullimcf  42258  addlimc  42283  limclner  42286  fourierdlem42  42784  fourierdlem80  42821  fourierdlem97  42838  sge0resplit  43038  volicorescl  43185  opnvonmbllem2  43265  smfaddlem1  43389  smflimlem6  43402  gbepos  44269  gbowpos  44270  gbegt5  44272  gboge9  44275
  Copyright terms: Public domain W3C validator