Theorem rexlimi 3256

Description: Restricted quantifier version of exlimi 2210. 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

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-ral 3062  df-rex 3071

This theorem is referenced by:  reuan  3889  triun  5279  reusv1  5394  reusv3  5402  iunopeqop  5520  tfinds  7845  fiun  7925  f1iun  7926  frpoins3xpg  8122  frpoins3xp3g  8123  iunfo  10530  iundom2g  10531  fsumcom2  15716  fprodcom2  15924  nosupbnd1  27206  nosupbnd2  27208  noinfbnd1  27221  noinfbnd2  27223  dfon2lem7  34749  finminlem  35191  r19.36vf  43810  allbutfiinf  44116  infxrunb3rnmpt  44124  hoidmvlelem1  45297  2zrngmmgm  46797