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

Theorem rexlimdvw 3150
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 3143 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061
This theorem is referenced by:  rspcebdv  3602  disjiund  5143  ralxfrd  5412  poxp3  8164  odi  8609  omeulem1  8612  qsss  8807  findcard3  9319  findcard3OLD  9320  ttrclselem2  9769  r1pwss  9827  dfac5lem4  10169  climuni  15554  rlimno1  15658  caurcvg2  15682  sscfn1  17833  gsumval2a  18678  gsumval3  19905  opnnei  23115  dislly  23492  lfinpfin  23519  txcmplem1  23636  ufileu  23914  alexsubALT  24046  metustel  24550  metustfbas  24557  i1faddlem  25713  ulmval  26409  brbtwn  28833  vtxduhgr0nedg  29429  wwlksnredwwlkn0  29830  midwwlks2s3  29886  umgr2cycl  34969  iccllysconn  35078  cvmopnlem  35106  cvmlift2lem10  35140  cvmlift3lem8  35154  sdclem2  37443  heibor1lem  37510  elrfi  42351  eldiophb  42414  dnnumch2  42706
  Copyright terms: Public domain W3C validator