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

Theorem rexlimi 3239
 Description: Restricted quantifier version of exlimi 2215. (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 3080 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3238 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 233 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3075  df-rex 3076 This theorem is referenced by:  reuan  3804  triun  5155  reusv1  5270  reusv3  5278  iunopeqop  5384  tfinds  7579  fiun  7654  f1iun  7655  iunfo  10012  iundom2g  10013  fsumcom2  15190  fprodcom2  15399  dfon2lem7  33293  frpoins3xpg  33344  frpoins3xp3g  33345  nosupbnd1  33514  nosupbnd2  33516  noinfbnd1  33529  noinfbnd2  33531  finminlem  34090  r19.36vf  42179  allbutfiinf  42458  infxrunb3rnmpt  42466  hoidmvlelem1  43635  2zrngmmgm  44986
 Copyright terms: Public domain W3C validator