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

Theorem rexlimi 3259
Description: Restricted quantifier version of exlimi 2217. For a version based on fewer axioms see rexlimiv 3148. (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 3063 . 2 𝑥𝐴 (𝜑𝜓)
3 rexlimi.1 . . 3 𝑥𝜓
43r19.23 3256 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
52, 4mpbi 230 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1783  wcel 2108  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3062  df-rex 3071
This theorem is referenced by:  reuan  3896  triun  5274  reusv1  5397  reusv3  5405  iunopeqop  5526  tfinds  7881  fiun  7967  f1iun  7968  frpoins3xpg  8165  frpoins3xp3g  8166  iunfo  10579  iundom2g  10580  fsumcom2  15810  fprodcom2  16020  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  dfon2lem7  35790  finminlem  36319  r19.36vf  45141  allbutfiinf  45431  infxrunb3rnmpt  45439  hoidmvlelem1  46610  2zrngmmgm  48168
  Copyright terms: Public domain W3C validator