Theorem rexlimi 3265

Description: Restricted quantifier version of exlimi 2255. For a version based on fewer axioms see rexlimiv 3159. (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 3081	. 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
3		rexlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	r19.23 3262	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
5	2, 4	mpbi 233	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1806   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-ral 3080  df-rex 3090

This theorem is referenced by:  reuan  3852  triun  5227  reusv1  5359  reusv3  5367  iunopeqop  5495  iunopeqopOLD  5496  tfinds  7844  fiun  7928  f1iun  7929  frpoins3xpg  8124  frpoins3xp3g  8125  iunfo  10511  iundom2g  10512  fsumcom2  15815  fprodcom2  16028  nosupbnd1  27836  nosupbnd2  27838  noinfbnd1  27851  noinfbnd2  27853  dfon2lem7  36150  finminlem  36691  r19.36vf  45712  allbutfiinf  45992  infxrunb3rnmpt  46000  hoidmvlelem1  47167  2zrngmmgm  48872