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

Theorem rexlimdvw 3016
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 3012 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902
This theorem is referenced by:  ralxfrd  4805  odi  7546  omeulem1  7549  qsss  7695  findcard3  8088  r1pwss  8530  dfac5lem4  8832  climuni  14131  rlimno1  14232  caurcvg2  14256  sscfn1  16300  gsumval2a  17102  gsumval3  18131  opnnei  20734  dislly  21110  lfinpfin  21137  txcmplem1  21254  ufileu  21533  alexsubALT  21665  metustel  22165  metustfbas  22172  i1faddlem  23266  ulmval  23938  brbtwn  25579  wwlknredwwlkn0  26255  iseupa  26492  iccllyscon  30486  cvmopnlem  30514  cvmlift2lem10  30548  cvmlift3lem8  30562  sdclem2  32708  heibor1lem  32778  elrfi  36275  eldiophb  36338  dnnumch2  36633  vtxduhgr0nedg  40707  wwlksnredwwlkn0  41102  elwwlks2ons3  41159  clwwlksnun  41281
  Copyright terms: Public domain W3C validator