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

Theorem rexlimdvv 3030
 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 453 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3023 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3024 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1987  ∃wrex 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2912  df-rex 2913 This theorem is referenced by:  rexlimdvva  3031  f1oiso2  6556  omeu  7610  xpdom2  7999  elfiun  8280  rankxplim3  8688  brdom6disj  9298  fpwwe2lem12  9407  tskxpss  9538  genpss  9770  genpcd  9772  genpnmax  9773  distrlem1pr  9791  distrlem5pr  9793  ltexprlem6  9807  reclem4pr  9816  supadd  10935  supmullem1  10937  supmullem2  10938  qaddcl  11748  qmulcl  11750  sqrlem6  13922  caubnd  14032  summo  14381  bezoutlem3  15182  bezoutlem4  15183  dvdsgcd  15185  gcddiv  15192  pceu  15475  pcqcl  15485  lspfixed  19047  lspexch  19048  lsmcv  19060  lspsolvlem  19061  hausnei2  21067  uncmp  21116  txcnp  21333  tx1stc  21363  fbasrn  21598  rnelfmlem  21666  blssps  22139  blss  22140  tgqioo  22511  ovolunlem2  23173  ax5seg  25718  axpasch  25721  axeuclid  25743  upgredg2vtx  25931  frgrwopreg  27044  pjhthmo  28007  shmodsi  28094  pjpjpre  28124  chscllem4  28345  sumdmdlem  29123  cdj3lem2a  29141  cdj3lem2b  29142  cdj3lem3a  29144  dya2iocnrect  30121  fprb  31370  noprefixmo  31570  btwndiff  31773  btwnconn1lem13  31845  btwnconn1lem14  31846  brsegle  31854  segletr  31860  segleantisym  31861  nn0prpwlem  31956  ismblfin  33079  heibor1lem  33237  crngohomfo  33434  lsmsat  33772  3dim1  34230  3dim3  34232  1cvratex  34236  atcvrlln2  34282  atcvrlln  34283  lplnnlelln  34306  llncvrlpln2  34320  lplnexllnN  34327  2llnjN  34330  lvolnlelln  34347  lvolnlelpln  34348  lplncvrlvol2  34378  2lplnj  34383  lneq2at  34541  lnatexN  34542  lncvrat  34545  lncmp  34546  paddasslem15  34597  paddasslem16  34598  pmodlem2  34610  pmapjoin  34615  llnexchb2  34632  lhp2lt  34764  cdlemf  35328  cdlemg1cex  35353  cdlemg2ce  35357  cdlemn11pre  35976  dihord2pre  35991  dihord4  36024  dihmeetlem20N  36092  mapdpglem24  36470  mapdpglem32  36471  baerlem3lem2  36476  baerlem5alem2  36477  baerlem5blem2  36478  hdmapglem7  36698  mzpcompact2lem  36791  pellex  36876  disjrnmpt2  38846  mullimc  39249  mullimcf  39256  addlimc  39281  limclner  39284  fourierdlem42  39670  fourierdlem80  39707  fourierdlem97  39724  sge0resplit  39927  volicorescl  40071  opnvonmbllem2  40151  smfaddlem1  40275  smflimlem6  40288  gbepos  40938  gbopos  40939  gbegt5  40941  gboage9  40944
 Copyright terms: Public domain W3C validator