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

Theorem rexlimdvw 3209
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 3202 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067
This theorem is referenced by:  rspcebdv  3531  disjiund  5043  ralxfrd  5301  odi  8307  omeulem1  8310  qsss  8460  findcard3  8914  r1pwss  9400  dfac5lem4  9740  climuni  15113  rlimno1  15217  caurcvg2  15241  sscfn1  17322  gsumval2a  18157  gsumval3  19292  opnnei  22017  dislly  22394  lfinpfin  22421  txcmplem1  22538  ufileu  22816  alexsubALT  22948  metustel  23448  metustfbas  23455  i1faddlem  24590  ulmval  25272  brbtwn  26990  vtxduhgr0nedg  27580  wwlksnredwwlkn0  27980  midwwlks2s3  28036  umgr2cycl  32816  iccllysconn  32925  cvmopnlem  32953  cvmlift2lem10  32987  cvmlift3lem8  33001  poxp3  33533  sdclem2  35637  heibor1lem  35704  elrfi  40219  eldiophb  40282  dnnumch2  40573
  Copyright terms: Public domain W3C validator