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

Theorem rexlimi 3319
Description: Restricted quantifier version of exlimi 2208. (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 3152 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3318 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 231 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1777  wcel 2106  wral 3142  wrex 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-ral 3147  df-rex 3148
This theorem is referenced by:  reuan  3883  triun  5181  reusv1  5293  reusv3  5301  iunopeqop  5407  tfinds  7565  fiunw  7635  f1iunw  7636  fiun  7638  f1iun  7639  iunfo  9953  iundom2g  9954  fsumcom2  15121  fprodcom2  15330  dfon2lem7  32919  nosupbnd1  33099  nosupbnd2  33101  finminlem  33551  r19.36vf  41266  allbutfiinf  41556  infxrunb3rnmpt  41564  hoidmvlelem1  42740  2zrngmmgm  44046
  Copyright terms: Public domain W3C validator