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

Theorem rexlimi 3006
 Description: Restricted quantifier version of exlimi 2073. (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 2906 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3004 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 219 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1699   ∈ wcel 1977  ∀wral 2896  ∃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  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902 This theorem is referenced by:  triun  4694  reusv1  4792  reusv1OLD  4793  reusv3  4802  iunopeqop  4906  tfinds  6951  fun11iun  7019  iunfo  9240  iundom2g  9241  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  dfon2lem7  30938  finminlem  31482  hoidmvlelem1  39485  reuan  39829  2zrngmmgm  41736
 Copyright terms: Public domain W3C validator