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

Theorem rexlimi 3053
Description: Restricted quantifier version of exlimi 2124. (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 2951 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3051 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 220 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1748  wcel 2030  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947
This theorem is referenced by:  triun  4799  reusv1  4896  reusv1OLD  4897  reusv3  4906  iunopeqop  5010  tfinds  7101  fun11iun  7168  iunfo  9399  iundom2g  9400  fsumcom2  14549  fsumcom2OLD  14550  fprodcom2  14758  fprodcom2OLD  14759  dfon2lem7  31818  nosupbnd1  31985  nosupbnd2  31987  finminlem  32437  r19.36vf  39638  allbutfiinf  39960  infxrunb3rnmpt  39968  hoidmvlelem1  41130  reuan  41501  2zrngmmgm  42271
  Copyright terms: Public domain W3C validator