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

Theorem rexlimi 3017
 Description: Restricted quantifier version of exlimi 2084. (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 2917 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3015 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 220 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1705   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-ral 2912  df-rex 2913 This theorem is referenced by:  triun  4726  reusv1  4826  reusv1OLD  4827  reusv3  4836  iunopeqop  4941  tfinds  7006  fun11iun  7073  iunfo  9305  iundom2g  9306  fsumcom2  14433  fsumcom2OLD  14434  fprodcom2  14639  fprodcom2OLD  14640  dfon2lem7  31392  finminlem  31951  r19.36vf  38811  allbutfiinf  39108  infxrunb3rnmpt  39116  hoidmvlelem1  40113  reuan  40481  2zrngmmgm  41231
 Copyright terms: Public domain W3C validator