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

Theorem rexlimdvw 3182
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 3178 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067
This theorem is referenced by:  rspcebdv  3465  disjiund  4777  ralxfrd  5008  odi  7811  omeulem1  7814  qsss  7958  findcard3  8357  r1pwss  8809  dfac5lem4  9147  climuni  14484  rlimno1  14585  caurcvg2  14609  sscfn1  16677  gsumval2a  17480  gsumval3  18508  opnnei  21138  dislly  21514  lfinpfin  21541  txcmplem1  21658  ufileu  21936  alexsubALT  22068  metustel  22568  metustfbas  22575  i1faddlem  23673  ulmval  24347  brbtwn  25993  vtxduhgr0nedg  26616  wwlksnredwwlkn0  27033  midwwlks2s3  27092  elwwlks2ons3OLD  27096  clwwlknunOLD  27286  iccllysconn  31563  cvmopnlem  31591  cvmlift2lem10  31625  cvmlift3lem8  31639  sdclem2  33863  heibor1lem  33933  elrfi  37776  eldiophb  37839  dnnumch2  38134
  Copyright terms: Public domain W3C validator