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

Theorem rexlimdvw 3063
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 3059 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  rspcebdv  3345  disjiund  4675  ralxfrd  4909  odi  7704  omeulem1  7707  qsss  7851  findcard3  8244  r1pwss  8685  dfac5lem4  8987  climuni  14327  rlimno1  14428  caurcvg2  14452  sscfn1  16524  gsumval2a  17326  gsumval3  18354  opnnei  20972  dislly  21348  lfinpfin  21375  txcmplem1  21492  ufileu  21770  alexsubALT  21902  metustel  22402  metustfbas  22409  i1faddlem  23505  ulmval  24179  brbtwn  25824  vtxduhgr0nedg  26444  wwlksnredwwlkn0  26859  midwwlks2s3  26917  elwwlks2ons3OLD  26921  clwwlknunOLD  27091  iccllysconn  31358  cvmopnlem  31386  cvmlift2lem10  31420  cvmlift3lem8  31434  sdclem2  33668  heibor1lem  33738  elrfi  37574  eldiophb  37637  dnnumch2  37932
  Copyright terms: Public domain W3C validator