Theorem rexlimi 3261

Description: Restricted quantifier version of exlimi 2251. For a version based on fewer axioms see rexlimiv 3155. (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

Step	Hyp	Ref	Expression
1		rexlimi.2	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	rgen 3077	. 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
3		rexlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	r19.23 3258	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
5	2, 4	mpbi 232	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1802   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-ral 3076  df-rex 3086

This theorem is referenced by:  reuan  3849  triun  5221  reusv1  5353  reusv3  5361  iunopeqop  5489  iunopeqopOLD  5490  tfinds  7836  fiun  7920  f1iun  7921  frpoins3xpg  8115  frpoins3xp3g  8116  iunfo  10493  iundom2g  10494  fsumcom2  15784  fprodcom2  15997  nosupbnd1  27755  nosupbnd2  27757  noinfbnd1  27770  noinfbnd2  27772  dfon2lem7  36101  finminlem  36642  r19.36vf  45678  allbutfiinf  45958  infxrunb3rnmpt  45966  hoidmvlelem1  47133  2zrngmmgm  48838