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

Theorem rexlimdvw 3249
 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 3242 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112 This theorem is referenced by:  rspcebdv  3565  disjiund  5021  ralxfrd  5275  odi  8191  omeulem1  8194  qsss  8344  findcard3  8748  r1pwss  9200  dfac5lem4  9540  climuni  14904  rlimno1  15005  caurcvg2  15029  sscfn1  17082  gsumval2a  17890  gsumval3  19024  opnnei  21735  dislly  22112  lfinpfin  22139  txcmplem1  22256  ufileu  22534  alexsubALT  22666  metustel  23167  metustfbas  23174  i1faddlem  24307  ulmval  24985  brbtwn  26703  vtxduhgr0nedg  27292  wwlksnredwwlkn0  27692  midwwlks2s3  27748  umgr2cycl  32516  iccllysconn  32625  cvmopnlem  32653  cvmlift2lem10  32687  cvmlift3lem8  32701  sdclem2  35199  heibor1lem  35266  elrfi  39678  eldiophb  39741  dnnumch2  40032
 Copyright terms: Public domain W3C validator