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

Theorem rexlimi 3312
Description: Restricted quantifier version of exlimi 2207. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Hypotheses
Ref Expression
rexlimi.1 𝑥𝜓
rexlimi.2 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexlimi (∃𝑥𝐴 𝜑𝜓)

Proof of Theorem rexlimi
StepHypRef Expression
1 rexlimi.2 . . 3 (𝑥𝐴 → (𝜑𝜓))
21rgen 3145 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3311 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 231 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1775  wcel 2105  wral 3135  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-ral 3140  df-rex 3141
This theorem is referenced by:  reuan  3877  triun  5176  reusv1  5288  reusv3  5296  iunopeqop  5402  tfinds  7563  fiun  7633  f1iun  7634  iunfo  9949  iundom2g  9950  fsumcom2  15117  fprodcom2  15326  dfon2lem7  32931  nosupbnd1  33111  nosupbnd2  33113  finminlem  33563  r19.36vf  41280  allbutfiinf  41570  infxrunb3rnmpt  41578  hoidmvlelem1  42754  2zrngmmgm  44145
  Copyright terms: Public domain W3C validator