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

Theorem rexlimdvw 3160
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvw.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rexlimdvw (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdvw
StepHypRef Expression
1 rexlimdvw.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3153 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071
This theorem is referenced by:  rspcebdv  3616  disjiund  5134  ralxfrd  5408  poxp3  8175  odi  8617  omeulem1  8620  qsss  8818  findcard3  9318  findcard3OLD  9319  ttrclselem2  9766  r1pwss  9824  dfac5lem4  10166  dfac5lem4OLD  10168  climuni  15588  rlimno1  15690  caurcvg2  15714  sscfn1  17861  gsumval2a  18698  gsumval3  19925  opnnei  23128  dislly  23505  lfinpfin  23532  txcmplem1  23649  ufileu  23927  alexsubALT  24059  metustel  24563  metustfbas  24570  i1faddlem  25728  ulmval  26423  brbtwn  28914  vtxduhgr0nedg  29510  wwlksnredwwlkn0  29916  midwwlks2s3  29972  umgr2cycl  35146  iccllysconn  35255  cvmopnlem  35283  cvmlift2lem10  35317  cvmlift3lem8  35331  sdclem2  37749  heibor1lem  37816  elrfi  42705  eldiophb  42768  dnnumch2  43057
  Copyright terms: Public domain W3C validator